harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Modular.lean
theorem eq_smul_self_of_mem_fdo_mem_fdo (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : z = g • z

Proof state:
case intro
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hg : T ^ n • z ∈ 𝒟ᵒ
hn : ∀ (z : ℍ), g • z = T ^ n • z
⊢ z = T ^ n • z

Tactic:
simp [eq_zero_of_mem_fdo_of_T_zpow_mem_fdo hz hg, one_smul]

Result:
no goals

Proof state:
case intro
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
n : ℤ
hn : ∀ (z : ℍ), g • z = T ^ n • z
⊢ z = g • z

Tactic:
rw [hn] at hg ⊢

Result:
case intro
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
n : ℤ
hg : T ^ n • z ∈ 𝒟ᵒ
hn : ∀ (z : ℍ), g • z = T ^ n • z
⊢ z = T ^ n • z

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ z = g • z

Tactic:
obtain ⟨n, hn⟩ := exists_eq_T_zpow_of_c_eq_zero (c_eq_zero hz hg)

Result:
case intro
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
n : ℤ
hn : ∀ (z : ℍ), g • z = T ^ n • z
⊢ z = g • z
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
private lemma comp_map (C' : VariableChange R) : (C.comp C').map φ = (C.map φ).comp (C'.map φ)

Proof state:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ map φ (C.comp C') = (map φ C).comp (map φ C')

Tactic:
simp only [comp, map]

Result:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
      t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) } =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
      s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
      t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }

Proof state:
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
      t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) } =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
      s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
      t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }

Tactic:
ext <;> map_simp <;> simp only [Units.coe_map, Units.coe_map_inv, MonoidHom.coe_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem rnDeriv_neg (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] :
    (-s).rnDeriv μ =ᵐ[μ] -s.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)

Tactic:
rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
  singularPart_add_withDensity_rnDeriv_eq]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ (-s).rnDeriv μ =ᶠ[ae μ] -s.rnDeriv μ

Tactic:
refine
  Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) (integrable_rnDeriv _ _).neg ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst✝ : s.HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
-- Mathlib/Data/Real/Sign.lean
theorem sign_of_neg {r : ℝ} (hr : r < 0) : sign r = -1

Proof state:
r : ℝ
hr : r < 0
⊢ r.sign = -1

Tactic:
rw [sign, if_pos hr]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem mul_star_self_ne_zero_iff (x : E) : x * x⋆ ≠ 0 ↔ x ≠ 0

Proof state:
E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
⊢ x * x⋆ ≠ 0 ↔ x ≠ 0

Tactic:
simp only [Ne, mul_star_self_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tendsto_sin_pi_div_two : Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)

Proof state:
case h.e'_5.h.e'_3

⊢ 1 = sin (π / 2)

Tactic:
simp

Result:
no goals

Proof state:
⊢ Tendsto sin (𝓝[<] (π / 2)) (𝓝 1)

Tactic:
convert continuous_sin.continuousWithinAt.tendsto

Result:
case h.e'_5.h.e'_3

⊢ 1 = sin (π / 2)
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_fst_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) :
    (hST.equiv g).fst = ⟨g, hg⟩

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g

Tactic:
rw [equiv, Equiv.ofBijective]

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ { toFun := fun x => ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨g, hg⟩, ⟨1, h1⟩) = g

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (hST.equiv g).1 = ⟨g, hg⟩

Tactic:
have : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g := by
  rw [equiv, Equiv.ofBijective]; simp

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
this : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
⊢ (hST.equiv g).1 = ⟨g, hg⟩

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ { toFun := fun x => ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨g, hg⟩, ⟨1, h1⟩) = g

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
this : hST.equiv.symm (⟨g, hg⟩, ⟨1, h1⟩) = g
⊢ (hST.equiv g).1 = ⟨g, hg⟩

Tactic:
conv_lhs => rw [← this, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem card_support (h : IsThreeCycle σ) : σ.support.card = 3

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ.support.card = 3

Tactic:
rw [← sum_cycleType, h.cycleType, Multiset.sum_singleton]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp)]
lemma isOfFinOrder_pow {n : ℕ} : IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Proof state:
case inr
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Tactic:
rcases Decidable.eq_or_ne n 0 with rfl | hn

Result:
case inl
G : Type u_1
inst✝ : Monoid G
a : G
⊢ IsOfFinOrder (a ^ 0) ↔ IsOfFinOrder a ∨ 0 = 0

case inr
G : Type u_1
inst✝ : Monoid G
a : G
n : ℕ
hn : n ≠ 0
⊢ IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Proof state:
case inl
G : Type u_1
inst✝ : Monoid G
a : G
⊢ IsOfFinOrder (a ^ 0) ↔ IsOfFinOrder a ∨ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem integral_condExp_indicator [mβ : MeasurableSpace β] {Y : α → β} (hY : Measurable Y)
    [SigmaFinite (μ.trim hY.comap_le)] {A : Set α} (hA : MeasurableSet A) :
    ∫ x, (μ[(A.indicator fun _ ↦ (1 : ℝ)) | mβ.comap Y]) x ∂μ = (μ A).toReal

Proof state:
α : Type u_1
β : Type u_2
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
Y : α → β
hY : Measurable Y
inst✝ : SigmaFinite (μ.trim ⋯)
A : Set α
hA : MeasurableSet A
⊢ ∫ (x : α), (μ[A.indicator fun x => 1|MeasurableSpace.comap Y mβ]) x ∂μ = (μ A).toReal

Tactic:
rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Teichmuller.lean
theorem teichmuller_mul_aux₁ {R : Type*} (x y : MvPolynomial R ℚ) :
    teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x * teichmullerFun p y)

Tactic:
rw [RingHom.map_mul]

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)

Proof state:
case a.h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
n : ℕ
⊢ ghostMap (teichmullerFun p (x * y)) n = (ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)) n

Tactic:
simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow]

Result:
no goals

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)

Tactic:
ext1 n

Result:
case a.h
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
n : ℕ
⊢ ghostMap (teichmullerFun p (x * y)) n = (ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)) n

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y

Tactic:
apply (ghostMap.bijective_of_invertible p (MvPolynomial R ℚ)).1

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x * teichmullerFun p y)
-- Mathlib/Data/List/Sublists.lean
theorem Pairwise.sublists' {R} :
    ∀ {l : List α}, Pairwise R l → Pairwise (Lex (swap R)) (sublists' l)
  | _, Pairwise.nil => pairwise_singleton _ _
  | _, @Pairwise.cons _ _ a l H₁ H₂ => by
    simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
      and_imp]
    refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩
    rintro l₁ sl₁ x l₂ _ rfl
    rcases l₁ with - | ⟨b, l₁⟩; · constructor
    exact Lex.rel (H₁ _ <| sl₁.subset <| mem_cons_self _ _)

Proof state:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
⊢ ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b

Tactic:
rintro l₁ sl₁ x l₂ _ rfl

Result:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
l₁ : List α
sl₁ : l₁ <+ l
l₂ : List α
a✝ : l₂ <+ l
⊢ Lex (swap R) l₁ (a :: l₂)

Proof state:
case nil
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (swap R) [] (a :: l₂)

Tactic:
constructor

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (swap R)) (a :: l).sublists'

Tactic:
simp only [sublists'_cons, pairwise_append, pairwise_map, mem_sublists', mem_map, exists_imp,
  and_imp]

Result:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (swap R)) l.sublists' ∧
    Pairwise (fun a_1 b => Lex (swap R) (a :: a_1) (a :: b)) l.sublists' ∧
      ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b

Proof state:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
l₁ : List α
sl₁ : l₁ <+ l
l₂ : List α
a✝ : l₂ <+ l
⊢ Lex (swap R) l₁ (a :: l₂)

Tactic:
rcases l₁ with - | ⟨b, l₁⟩

Result:
case nil
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
sl₁ : [] <+ l
⊢ Lex (swap R) [] (a :: l₂)

case cons
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (swap R) (b :: l₁) (a :: l₂)

Proof state:
case cons
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
l₂ : List α
a✝ : l₂ <+ l
b : α
l₁ : List α
sl₁ : b :: l₁ <+ l
⊢ Lex (swap R) (b :: l₁) (a :: l₂)

Tactic:
exact Lex.rel (H₁ _ <| sl₁.subset <| mem_cons_self _ _)

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
⊢ Pairwise (Lex (swap R)) l.sublists' ∧
    Pairwise (fun a_1 b => Lex (swap R) (a :: a_1) (a :: b)) l.sublists' ∧
      ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b

Tactic:
refine ⟨H₂.sublists', H₂.sublists'.imp fun l₁ => Lex.cons l₁, ?_⟩

Result:
α : Type u
R : α → α → Prop
a : α
l : List α
H₁ : ∀ a' ∈ l, R a a'
H₂ : Pairwise R l
⊢ ∀ (a_1 : List α), a_1 <+ l → ∀ (b x : List α), x <+ l → a :: x = b → Lex (swap R) a_1 b
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem eq_of_forall_apply_eq (μ ν : FiniteMeasure Ω)
    (h : ∀ s : Set Ω, MeasurableSet s → μ s = ν s) : μ = ν

Proof state:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s

Tactic:
simpa [ennreal_coeFn_eq_coeFn_toMeasure] using congr_arg ((↑) : ℝ≥0 → ℝ≥0∞) (h s s_mble)

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
⊢ μ = ν

Tactic:
ext1 s s_mble

Result:
case h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → μ s = ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma complexMGF_ofReal (x : ℝ) : complexMGF X μ x = mgf X μ x

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ complexMGF X μ ↑x = ↑(mgf X μ x)

Tactic:
rw [complexMGF, mgf, ← integral_complex_ofReal]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ ∫ (x_1 : Ω), (fun ω => cexp (↑x * ↑(X ω))) x_1 ∂μ = ∫ (x_1 : Ω), ↑(rexp (x * X x_1)) ∂μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ ∫ (x_1 : Ω), (fun ω => cexp (↑x * ↑(X ω))) x_1 ∂μ = ∫ (x_1 : Ω), ↑(rexp (x * X x_1)) ∂μ

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem reverse_reverse (s : Cycle α) : s.reverse.reverse = s :=
  Quot.inductionOn s fun _ => by simp

Proof state:
α : Type u_1
s : Cycle α
x✝ : List α
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α)) x✝)).reverse = Quot.mk (⇑(IsRotated.setoid α)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma triangle_aux₂ {X Y  : LocalizedMonoidal L W ε} {X' Y' : C}
    (e₁ : (L').obj X' ≅ X) (e₂ : (L').obj Y' ≅ Y) :
      e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom =
        (L').obj X' ◁ ((ε' L W ε).hom ▷ (L').obj Y' ≫
          𝟙_ _ ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

Proof state:
case e_g.e_a.e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ ε.hom = (ε' L W ε).hom ≫ 𝟙 (𝟙_ (LocalizedMonoidal L W ε))

Tactic:
exact (comp_id _).symm

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom =
    e₁.hom ⊗ ((ε' L W ε).hom ≫ 𝟙 (𝟙_ (LocalizedMonoidal L W ε)) ⊗ e₂.hom) ≫ (λ_ Y).hom

Tactic:
congr 3

Result:
case e_g.e_a.e_f
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ ε.hom = (ε' L W ε).hom ≫ 𝟙 (𝟙_ (LocalizedMonoidal L W ε))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom =
    L'.obj X' ◁ ((ε' L W ε).hom ▷ L'.obj Y' ≫ 𝟙_ (LocalizedMonoidal L W ε) ◁ e₂.hom ≫ (λ_ Y).hom) ≫ e₁.hom ▷ Y

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, comp_id, id_comp,
  ← tensor_comp_assoc, id_comp]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : L'.obj X' ≅ X
e₂ : L'.obj Y' ≅ Y
⊢ e₁.hom ⊗ (ε.hom ⊗ e₂.hom) ≫ (λ_ Y).hom =
    e₁.hom ⊗ ((ε' L W ε).hom ≫ 𝟙 (𝟙_ (LocalizedMonoidal L W ε)) ⊗ e₂.hom) ≫ (λ_ Y).hom
-- Mathlib/Order/Height.lean
theorem chainHeight_eq_iSup_Iic : s.chainHeight = ⨆ i ∈ s, (s ∩ Set.Iic i).chainHeight

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ s.chainHeight = ⨆ i ∈ s, (s ∩ Iic i).chainHeight

Tactic:
simp_rw [← chainHeight_dual (_ ∩ _)]

Result:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ s.chainHeight = ⨆ i ∈ s, (⇑ofDual ⁻¹' (s ∩ Iic i)).chainHeight

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ s.chainHeight = ⨆ i ∈ s, (⇑ofDual ⁻¹' (s ∩ Iic i)).chainHeight

Tactic:
rw [← chainHeight_dual, chainHeight_eq_iSup_Ici]

Result:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ ⨆ i ∈ ⇑ofDual ⁻¹' s, (⇑ofDual ⁻¹' s ∩ Ici i).chainHeight = ⨆ i ∈ s, (⇑ofDual ⁻¹' (s ∩ Iic i)).chainHeight

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ ⨆ i ∈ ⇑ofDual ⁻¹' s, (⇑ofDual ⁻¹' s ∩ Ici i).chainHeight = ⨆ i ∈ s, (⇑ofDual ⁻¹' (s ∩ Iic i)).chainHeight

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk_eq_mk'_apply (x y) : mk x y = IsLocalization.mk' (Localization M) x y

Proof state:
R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
x : R
y : ↥M
⊢ mk x y = mk' (Localization M) x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.size_tail?_lt {s : Heap α} : s.tail? le = some s' →
    s'.size < s.size

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s'.size < s.size

Tactic:
intro eq

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s'.size < s.size

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
a : α
tl : Heap α
eq₂ : deleteMin le s = some (a, tl)
⊢ ((fun x => x.snd) (a, tl)).size < s.size

Tactic:
exact size_deleteMin_lt eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s'.size < s.size

Tactic:
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact size_deleteMin_lt eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ tail? le s = some s' → s'.size < s.size

Tactic:
simp only [Heap.tail?]

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s'.size < s.size
-- Mathlib/Algebra/GroupWithZero/Center.lean
lemma center_units_subset : center G₀ˣ ⊆ ((↑) : G₀ˣ → G₀) ⁻¹' center G₀

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * ↑x = ↑x * g

Tactic:
intro u hu a

Result:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
⊢ a * ↑u = ↑u * a

Proof state:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0

Tactic:
rw [zero_mul, mul_zero]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ center G₀ˣ ⊆ Units.val ⁻¹' center G₀

Tactic:
simp_rw [subset_def, mem_preimage, _root_.Semigroup.mem_center_iff]

Result:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (x : G₀ˣ), (∀ (g : G₀ˣ), g * x = x * g) → ∀ (g : G₀), g * ↑x = ↑x * g

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
⊢ a * ↑u = ↑u * a

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 * ↑u = ↑u * 0

case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a

Proof state:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
a : G₀
ha : a ≠ 0
⊢ a * ↑u = ↑u * a

Tactic:
exact congr_arg Units.val <| hu <| Units.mk0 a ha

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_le_two_mul (ha : 2⁻¹ ≤ a) : ⌈a⌉ ≤ 2 * a :=
  ceil_le_mul one_lt_two (by norm_num at ha ⊢; exact ha)

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 2⁻¹ ≤ a
⊢ ↑⌈(2 - 1)⁻¹⌉ / 2 ≤ a

Tactic:
norm_num at ha ⊢

Result:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
exact ha

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Vector/Monadic.lean
theorem mapM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
    (a : Array α) (h : a.size = n) (f : α → m β) :
    (Vector.mk a h).mapM f =
      (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying (Array.size_mapM f a)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : α → m β
⊢ mapM f { toArray := a, size_toArray := h } =
    (fun x =>
        match x with
        | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
      satisfying ⋯

Tactic:
rw [← LawfulMonad.map_inj_right Vector.toArray_inj.mp]

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : α → m β
⊢ (fun {x} => x.toArray) <$> mapM f { toArray := a, size_toArray := h } =
    (fun {x} => x.toArray) <$>
      (fun x =>
          match x with
          | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
        satisfying ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : α → m β
⊢ (fun {x} => x.toArray) <$> mapM f { toArray := a, size_toArray := h } =
    (fun {x} => x.toArray) <$>
      (fun x =>
          match x with
          | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
        satisfying ⋯

Tactic:
simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapM]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem injective_of_top_hom (f : (⊤ : SimpleGraph V) →g G') : Function.Injective f

Proof state:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v w : V
h : f v = f w
⊢ v = w

Tactic:
contrapose! h

Result:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v w : V
h : v ≠ w
⊢ f v ≠ f w

Proof state:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v w : V
h : v ≠ w
⊢ f v ≠ f w

Tactic:
exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
⊢ Injective ⇑f

Tactic:
intro v w h

Result:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : ⊤ →g G'
v w : V
h : f v = f w
⊢ v = w