harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
theorem choose_choose_eq_of_mapsTo :
    (exist_eq_reflection_of_mapsTo p root coroot i
      (exist_eq_reflection_of_mapsTo p root coroot i j h).choose h).choose = j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2
⊢ (preReflection (root i) (p.flip (coroot i))) ((preReflection (root i) (p.flip (coroot i))) (root j)) = root j

Tactic:
apply involutive_preReflection (x := root i) (hp i)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2
⊢ ⋯.choose = j

Tactic:
refine root.injective ?_

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2
⊢ root ⋯.choose = root j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2
⊢ root ⋯.choose = root j

Tactic:
rw [(exist_eq_reflection_of_mapsTo p root coroot i _ h).choose_spec,
  (exist_eq_reflection_of_mapsTo p root coroot i j h).choose_spec]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
root : ι ↪ M
coroot : ι ↪ N
i j : ι
h : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)
hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2
⊢ (preReflection (root i) (p.flip (coroot i))) ((preReflection (root i) (p.flip (coroot i))) (root j)) = root j
-- Mathlib/Data/Finset/Card.lean
theorem exists_ne_of_one_lt_card (hs : 1 < #s) (a : α) : ∃ b, b ∈ s ∧ b ≠ a

Proof state:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ ∃ b ∈ s, b ≠ a

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp hs

Result:
case intro.intro.intro.intro
α : Type u_1
s : Finset α
hs : 1 < #s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ b ∈ s, b ≠ a

Proof state:
case intro.intro.intro.intro
α : Type u_1
s : Finset α
hs : 1 < #s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_cases ha : y = a

Result:
case pos
α : Type u_1
s : Finset α
hs : 1 < #s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : y = a
⊢ ∃ b ∈ s, b ≠ a

case neg
α : Type u_1
s : Finset α
hs : 1 < #s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : ¬y = a
⊢ ∃ b ∈ s, b ≠ a

Proof state:
case pos
α : Type u_1
s : Finset α
hs : 1 < #s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : y = a
⊢ ∃ b ∈ s, b ≠ a

Tactic:
exact ⟨x, hx, ne_of_ne_of_eq hxy ha⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
s : Finset α
hs : 1 < #s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : ¬y = a
⊢ ∃ b ∈ s, b ≠ a

Tactic:
exact ⟨y, hy, ha⟩

Result:
no goals
-- Mathlib/Topology/JacobsonSpace.lean
lemma JacobsonSpace.of_isOpenEmbedding [JacobsonSpace Y] (hf : IsOpenEmbedding f) :
    JacobsonSpace X

Proof state:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ JacobsonSpace X

Tactic:
rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]

Result:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Proof state:
case intro.intro.intro.intro
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
exact ⟨_, hx, hx'⟩

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
⊢ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
intros Z hZ hZ'

Result:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Proof state:
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty

Tactic:
obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ := nonempty_inter_closedPoints
  (hZ.image f) (hZ'.image hf.isInducing hf.isOpen_range.isLocallyClosed)

Result:
case intro.intro.intro.intro
X : Type u_2
Y : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : JacobsonSpace Y
hf : IsOpenEmbedding f
Z : Set X
hZ : Z.Nonempty
hZ' : IsLocallyClosed Z
x : X
hx : x ∈ Z
hx' : f x ∈ closedPoints Y
⊢ (Z ∩ f ⁻¹' closedPoints Y).Nonempty
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.rec' [Mul R] [Add R] [Zero R]
    {motive : (s : R) → (h : IsSumSq s) → Prop}
    (zero : motive 0 zero)
    (sq_add : ∀ {x s}, (hx : IsSquare x) → (hs : IsSumSq s) → motive s hs →
      motive (x + s) (by rcases hx with ⟨_, rfl⟩; exact sq_add _ hs))
    {s : R} (h : IsSumSq s) : motive s h :=
  match h with
  | .zero        => zero
  | .sq_add _ hs => sq_add (.mul_self _) hs (rec' zero sq_add _)

Proof state:
case intro
R : Type u_1
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Zero R
motive : (s : R) → IsSumSq s → Prop
zero : motive 0 ⋯
s : R
hs : IsSumSq s
w✝ : R
⊢ IsSumSq (w✝ * w✝ + s)

Tactic:
exact sq_add _ hs

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Zero R
motive : (s : R) → IsSumSq s → Prop
zero : motive 0 ⋯
x s : R
hx : IsSquare x
hs : IsSumSq s
⊢ IsSumSq (x + s)

Tactic:
rcases hx with ⟨_, rfl⟩

Result:
case intro
R : Type u_1
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : Zero R
motive : (s : R) → IsSumSq s → Prop
zero : motive 0 ⋯
s : R
hs : IsSumSq s
w✝ : R
⊢ IsSumSq (w✝ * w✝ + s)
-- Mathlib/RingTheory/Multiplicity.lean
theorem min_le_emultiplicity_add {p a b : α} :
    min (emultiplicity p a) (emultiplicity p b) ≤ emultiplicity p (a + b)

Proof state:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Tactic:
exact hm.or_of_add

Result:
no goals

Proof state:
case coe.hk
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : emultiplicity p a ⊓ emultiplicity p b = ↑a✝
⊢ p ^ a✝ ∣ a + b

Tactic:
simp [dvd_add, pow_dvd_of_le_emultiplicity, ← hm]

Result:
no goals

Proof state:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : ¬¬FiniteMultiplicity p (a + b)
⊢ ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)

Tactic:
simp only [not_and_or, not_not] at hm ⊢

Result:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : FiniteMultiplicity p (a + b)
⊢ FiniteMultiplicity p a ∨ FiniteMultiplicity p b

Proof state:
α : Type u_1
inst✝ : Semiring α
p a b : α
⊢ emultiplicity p a ⊓ emultiplicity p b ≤ emultiplicity p (a + b)

Tactic:
cases hm : min (emultiplicity p a) (emultiplicity p b)

Result:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : emultiplicity p a ⊓ emultiplicity p b = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : emultiplicity p a ⊓ emultiplicity p b = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)

Proof state:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ ¬FiniteMultiplicity p (a + b)

Tactic:
contrapose hm

Result:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : ¬¬FiniteMultiplicity p (a + b)
⊢ ¬(¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b)

Proof state:
case coe
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : emultiplicity p a ⊓ emultiplicity p b = ↑a✝
⊢ ↑a✝ ≤ emultiplicity p (a + b)

Tactic:
apply le_emultiplicity_of_pow_dvd

Result:
case coe.hk
α : Type u_1
inst✝ : Semiring α
p a b : α
a✝ : ℕ
hm : emultiplicity p a ⊓ emultiplicity p b = ↑a✝
⊢ p ^ a✝ ∣ a + b

Proof state:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : emultiplicity p a ⊓ emultiplicity p b = ⊤
⊢ ⊤ ≤ emultiplicity p (a + b)

Tactic:
simp only [top_le_iff, min_eq_top, emultiplicity_eq_top] at hm ⊢

Result:
case top
α : Type u_1
inst✝ : Semiring α
p a b : α
hm : ¬FiniteMultiplicity p a ∧ ¬FiniteMultiplicity p b
⊢ ¬FiniteMultiplicity p (a + b)
-- Mathlib/Order/Filter/Partial.lean
theorem rtendsto'_def (r : Rel α β) (l₁ : Filter α) (l₂ : Filter β) :
    RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁

Proof state:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => r.preimage s ⊆ t) l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
constructor

Result:
case mp
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => r.preimage s ⊆ t) l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } →
    ∀ s ∈ l₂, r.preimage s ∈ l₁

case mpr
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.preimage s ∈ l₁) →
    l₁ ≤
      { sets := Rel.image (fun s t => r.preimage s ⊆ t) l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ }

Proof state:
case mp
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => r.preimage s ⊆ t) l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } →
    ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
simpa [le_def, Rel.mem_image] using fun h s hs => h _ _ hs Set.Subset.rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ RTendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁

Tactic:
unfold RTendsto' rcomap'

Result:
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ l₁ ≤
      { sets := Rel.image (fun s t => r.preimage s ⊆ t) l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ } ↔
    ∀ s ∈ l₂, r.preimage s ∈ l₁

Proof state:
case mpr
α : Type u
β : Type v
r : Rel α β
l₁ : Filter α
l₂ : Filter β
⊢ (∀ s ∈ l₂, r.preimage s ∈ l₁) →
    l₁ ≤
      { sets := Rel.image (fun s t => r.preimage s ⊆ t) l₂.sets, univ_sets := ⋯, sets_of_superset := ⋯,
        inter_sets := ⋯ }

Tactic:
simpa [le_def, Rel.mem_image] using fun h s t ht => mem_of_superset (h t ht)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem natDegree_modByMonic_lt (p : R[X]) {q : R[X]} (hmq : Monic q) (hq : q ≠ 1) :
    natDegree (p %ₘ q) < q.natDegree

Proof state:
case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
this : Nontrivial R
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
haveI := Nontrivial.of_polynomial_ne hpq

Result:
case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
this : Nontrivial R
⊢ (p %ₘ q).natDegree < q.natDegree

Proof state:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ q.natDegree ≠ 0

Tactic:
contrapose! hq

Result:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hpq : p %ₘ q = 0
hq : q.natDegree = 0
⊢ q = 1

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
by_cases hpq : p %ₘ q = 0

Result:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

case neg
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

Proof state:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]

Result:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ q.natDegree ≠ 0

Proof state:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
hmq : q.Monic
hpq : p %ₘ q = 0
hq : q.natDegree = 0
⊢ q = 1

Tactic:
exact eq_one_of_monic_natDegree_zero hmq hq

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
/-- A point-free means of proving membership in the center, for a non-associative ring.

This can be helpful when working with types that have ext lemmas for `R →+ R`. -/
lemma _root_.Set.mem_center_iff_addMonoidHom (a : R) :
    a ∈ Set.center R ↔
      AddMonoidHom.mulLeft a = .mulRight a ∧
      AddMonoidHom.compr₂ .mul (.mulLeft a) = .comp .mul (.mulLeft a) ∧
      AddMonoidHom.comp .mul (.mulRight a) = .compl₂ .mul (.mulLeft a) ∧
      AddMonoidHom.compr₂ .mul (.mulRight a) = .compl₂ .mul (.mulRight a)

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ a ∈ Set.center R ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧
          AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Tactic:
rw [Set.mem_center_iff, isMulCentral_iff]

Result:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ ((∀ (a_1 : R), a * a_1 = a_1 * a) ∧
      (∀ (b c : R), a * (b * c) = a * b * c) ∧
        (∀ (a_1 c : R), a_1 * a * c = a_1 * (a * c)) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧
          AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
a : R
⊢ ((∀ (a_1 : R), a * a_1 = a_1 * a) ∧
      (∀ (b c : R), a * (b * c) = a * b * c) ∧
        (∀ (a_1 c : R), a_1 * a * c = a_1 * (a * c)) ∧ ∀ (a_1 b : R), a_1 * b * a = a_1 * (b * a)) ↔
    AddMonoidHom.mulLeft a = AddMonoidHom.mulRight a ∧
      AddMonoidHom.mul.compr₂ (AddMonoidHom.mulLeft a) = AddMonoidHom.mul.comp (AddMonoidHom.mulLeft a) ∧
        AddMonoidHom.mul.comp (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulLeft a) ∧
          AddMonoidHom.mul.compr₂ (AddMonoidHom.mulRight a) = AddMonoidHom.mul.compl₂ (AddMonoidHom.mulRight a)

Tactic:
simp [DFunLike.ext_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem boundedAtFilter_cuspFunction (hh : 0 < h) (h_bd : BoundedAtFilter I∞ f) :
    BoundedAtFilter (𝓝[≠] 0) (cuspFunction h f)

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
q : ℂ
hq : q ∈ {0}ᶜ
⊢ (f ∘ invQParam h) q = cuspFunction h f q

Tactic:
rw [cuspFunction_eq_of_nonzero _ _ hq, comp_def]

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ 1 ∘ invQParam h =ᶠ[𝓝[≠] 0] 1

Tactic:
rfl

Result:
no goals

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ f ∘ invQParam h =ᶠ[𝓝[≠] 0] cuspFunction h f

Tactic:
refine eventually_nhdsWithin_of_forall fun q hq ↦ ?_

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
q : ℂ
hq : q ∈ {0}ᶜ
⊢ (f ∘ invQParam h) q = cuspFunction h f q

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ (𝓝[≠] 0).BoundedAtFilter (cuspFunction h f)

Tactic:
refine (h_bd.comp_tendsto <| invQParam_tendsto hh).congr' ?_ (by rfl)

Result:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_bd : I∞.BoundedAtFilter f
⊢ f ∘ invQParam h =ᶠ[𝓝[≠] 0] cuspFunction h f
-- Mathlib/Data/Set/Function.lean
theorem piecewise_singleton (x : α) [∀ y, Decidable (y ∈ ({x} : Set α))] [DecidableEq α]
    (f g : α → β) : piecewise {x} f g = Function.update g x (f x)

Proof state:
case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g x = update g x (f x) x

Tactic:
simp

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
simp [hy]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
by_cases hy : y = x

Result:
case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ {x}.piecewise f g y = update g x (f x) y

case neg
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : ¬y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Proof state:
case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
hy : y = x
⊢ {x}.piecewise f g y = update g x (f x) y

Tactic:
subst y

Result:
case pos
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g x = update g x (f x) x

Proof state:
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
⊢ {x}.piecewise f g = update g x (f x)

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
x : α
inst✝¹ : (y : α) → Decidable (y ∈ {x})
inst✝ : DecidableEq α
f g : α → β
y : α
⊢ {x}.piecewise f g y = update g x (f x) y
-- Mathlib/Algebra/Group/Subgroup/MulOppositeLemmas.lean
theorem unop_closure (s : Set Gᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]

Result:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Proof state:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem smtSDiv_eq (x y : BitVec w) : smtSDiv x y =
  match x.msb, y.msb with
  | false, false => smtUDiv x y
  | false, true  => -(smtUDiv x (-y))
  | true,  false => -(smtUDiv (-x) y)
  | true,  true  => smtUDiv (-x) (-y)

Proof state:
w : Nat
x y : BitVec w
⊢ x.smtSDiv y =
    match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => -x.smtUDiv (-y)
    | true, false => -(-x).smtUDiv y
    | true, true => (-x).smtUDiv (-y)

Tactic:
rw [BitVec.smtSDiv]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => (x.smtUDiv y.neg).neg
    | true, false => (x.neg.smtUDiv y).neg
    | true, true => x.neg.smtUDiv y.neg) =
    match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => -x.smtUDiv (-y)
    | true, false => -(-x).smtUDiv y
    | true, true => (-x).smtUDiv (-y)

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => (x.smtUDiv y.neg).neg
    | true, false => (x.neg.smtUDiv y).neg
    | true, true => x.neg.smtUDiv y.neg) =
    match x.msb, y.msb with
    | false, false => x.smtUDiv y
    | false, true => -x.smtUDiv (-y)
    | true, false => -(-x).smtUDiv y
    | true, true => (-x).smtUDiv (-y)

Tactic:
rcases x.msb <;> rcases y.msb <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mk₂_surjective (X : ComposableArrows C 2) :
    ∃ (X₀ X₁ X₂ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂), X = mk₂ f₀ f₁ :=
  ⟨_, _, _, X.map' 0 1, X.map' 1 2, ext₂ rfl rfl rfl (by simp) (by simp)⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 2
⊢ X.map' 1 2 ⋯ ⋯ = eqToHom ⋯ ≫ (mk₂ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯)).map' 1 2 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 2
⊢ X.map' 0 1 ⋯ ⋯ = eqToHom ⋯ ≫ (mk₂ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem symm_trans_self (h : X ≃ₜ Y) : h.symm.trans h = Homeomorph.refl Y

Proof state:
case H
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : Y
⊢ (h.symm.trans h) x✝ = (Homeomorph.refl Y) x✝

Tactic:
apply apply_symm_apply

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.symm.trans h = Homeomorph.refl Y

Tactic:
ext

Result:
case H
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : Y
⊢ (h.symm.trans h) x✝ = (Homeomorph.refl Y) x✝
-- Mathlib/GroupTheory/CoprodI.lean
theorem prod_rcons {i} (p : Pair M i) : prod (rcons p) = of p.head * prod p.tail :=
  if hm : p.head = 1 then by rw [rcons, dif_pos hm, hm, MonoidHom.map_one, one_mul]
  else by rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : p.head = 1
⊢ (rcons p).prod = of p.head * p.tail.prod

Tactic:
rw [rcons, dif_pos hm, hm, MonoidHom.map_one, one_mul]

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
p : Pair M i
hm : ¬p.head = 1
⊢ (rcons p).prod = of p.head * p.tail.prod

Tactic:
rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]

Result:
no goals