α : Type u_1
β : Type u_2
γ : Type ?u.2439120
δ : Type ?u.2439123
ι : Type ?u.2439126
R : Type ?u.2439129
R' : Type ?u.2439132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
μ₁ μ₂ : MeasureTheory.Measure α
hμ : Measure.map (↑e) μ₁ = Measure.map (↑e) μ₂
⊢ μ₁ = μ₂
α : Type u_1
β : Type u_2
γ : Type ?u.2439120
δ : Type ?u.2439123
ι : Type ?u.2439126
R : Type ?u.2439129
R' : Type ?u.2439132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
⊢ Injective (Measure.map ↑e)
intro μ₁ μ₂ hμ
α : Type u_1
β : Type u_2
γ : Type ?u.2439120
δ : Type ?u.2439123
ι : Type ?u.2439126
R : Type ?u.2439129
R' : Type ?u.2439132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
μ₁ μ₂ : MeasureTheory.Measure α
hμ : Measure.map (↑(symm e)) (Measure.map (↑e) μ₁) = Measure.map (↑(symm e)) (Measure.map (↑e) μ₂)
⊢ μ₁ = μ₂
α : Type u_1
β : Type u_2
γ : Type ?u.2439120
δ : Type ?u.2439123
ι : Type ?u.2439126
R : Type ?u.2439129
R' : Type ?u.2439132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
μ₁ μ₂ : MeasureTheory.Measure α
hμ : Measure.map (↑e) μ₁ = Measure.map (↑e) μ₂
⊢ μ₁ = μ₂
apply_fun Measure.map e.symm  at hμ
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.2439120
δ : Type ?u.2439123
ι : Type ?u.2439126
R : Type ?u.2439129
R' : Type ?u.2439132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : MeasureTheory.Measure α
ν : MeasureTheory.Measure β
e : α ≃ᵐ β
μ₁ μ₂ : MeasureTheory.Measure α
hμ : Measure.map (↑(symm e)) (Measure.map (↑e) μ₁) = Measure.map (↑(symm e)) (Measure.map (↑e) μ₂)
⊢ μ₁ = μ₂
simpa [map_symm_map e] using hμ