harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/FreeMonoid/Basic.lean
theorem hom_eq ⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
  MonoidHom.ext fun l ↦ recOn l (f.map_one.trans g.map_one.symm)
    (fun x xs hxs ↦ by simp only [h, hxs, MonoidHom.map_mul])

Proof state:
α : Type u_1
M : Type u_4
inst✝ : Monoid M
f g : FreeMonoid α →* M
h : ∀ (x : α), f (of x) = g (of x)
l : FreeMonoid α
x : α
xs : FreeMonoid α
hxs : f xs = g xs
⊢ f (of x * xs) = g (of x * xs)

Tactic:
simp only [h, hxs, MonoidHom.map_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Action.lean
theorem smul_set_ae_le (c : G) {s t : Set α} : c • s ≤ᵐ[μ] c • t ↔ s ≤ᵐ[μ] t

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ c • s ≤ᶠ[ae μ] c • t ↔ s ≤ᶠ[ae μ] t

Tactic:
simp only [ae_le_set, ← smul_set_sdiff, measure_smul_eq_zero_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_add_pi_div_two (x : ℂ) : sin (x + π / 2) = cos x

Proof state:
x : ℂ
⊢ sin (x + ↑π / 2) = cos x

Tactic:
simp [sin_add]

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma gc_exterior_interior : GaloisConnection (exterior : Set α → Set α) interior :=
  fun s t ↦ by simp [exterior_subset_iff, subset_interior_iff]

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s t : Set α
⊢ exterior s ≤ t ↔ s ≤ interior t

Tactic:
simp [exterior_subset_iff, subset_interior_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem ordConnectedComponent_inter (s t : Set α) (x : α) :
    ordConnectedComponent (s ∩ t) x = ordConnectedComponent s x ∩ ordConnectedComponent t x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
x : α
⊢ (s ∩ t).ordConnectedComponent x = s.ordConnectedComponent x ∩ t.ordConnectedComponent x

Tactic:
simp [ordConnectedComponent, setOf_and]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Factorization.lean
@[reassoc (attr := simp)]
lemma fac_app {f : Arrow C} : data.i.app f ≫ data.p.app f = f.hom

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ data.i.app f ≫ data.p.app f = f.hom

Tactic:
rw [← NatTrans.comp_app, fac,Arrow.leftToRight_app]

Result:
no goals
-- Mathlib/Algebra/ZeroOne/Lemmas.lean
@[to_additive]
lemma ite_lt_one [LT α] (ha : a < 1) (hb : b < 1) : ite p a b < 1

Proof state:
α : Type u_1
inst✝² : One α
p : Prop
inst✝¹ : Decidable p
a b : α
inst✝ : LT α
ha : a < 1
hb : b < 1
⊢ (if p then a else b) < 1

Tactic:
split <;> assumption

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_natCast (n : Nat) : withTopEquiv n = n

Proof state:
n : ℕ
⊢ withTopEquiv ↑n = ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem iInf_neBot_of_directed' {f : ι → Filter α} [Nonempty ι] (hd : Directed (· ≥ ·) f) :
    (∀ i, NeBot (f i)) → NeBot (iInf f) :=
  not_imp_not.1 <| by simpa only [not_forall, not_neBot, ← empty_mem_iff_bot,
    mem_iInf_of_directed hd] using id

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
inst✝ : Nonempty ι
hd : Directed (fun x1 x2 => x1 ≥ x2) f
⊢ ¬(iInf f).NeBot → ¬∀ (i : ι), (f i).NeBot

Tactic:
simpa only [not_forall, not_neBot, ← empty_mem_iff_bot,
mem_iInf_of_directed hd] using id

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem iso_inv_image_comp_eq_iff_eq_map {C : G.ConnectedComponent} :
    G.connectedComponentMk (φ.symm v') = C ↔ G'.connectedComponentMk v' = C.map φ

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v' : V'
C : G.ConnectedComponent
⊢ G.connectedComponentMk (φ.symm v') = C ↔ G'.connectedComponentMk v' = map (RelIso.toRelEmbedding φ).toRelHom C

Tactic:
refine C.ind fun u => ?_

Result:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v' : V'
C : G.ConnectedComponent
u : V
⊢ G.connectedComponentMk (φ.symm v') = G.connectedComponentMk u ↔
    G'.connectedComponentMk v' = map (RelIso.toRelEmbedding φ).toRelHom (G.connectedComponentMk u)

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
v' : V'
C : G.ConnectedComponent
u : V
⊢ G.connectedComponentMk (φ.symm v') = G.connectedComponentMk u ↔
    G'.connectedComponentMk v' = map (RelIso.toRelEmbedding φ).toRelHom (G.connectedComponentMk u)

Tactic:
simp only [Iso.symm_apply_reachable, ConnectedComponent.eq, ConnectedComponent.map_mk,
  RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)

Proof state:
case succ
n k : ℕ
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
obtain hk | hk := le_or_lt (k + 1) (n + 1)

Result:
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Proof state:
case zero
n : ℕ
⊢ n.choose 0 * (n + 1) = (n + 1).choose 0 * (n + 1 - 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ.inr
n k : ℕ
hk : n + 1 < k + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
  Nat.zero_mul]

Result:
no goals

Proof state:
case succ.inl
n k : ℕ
hk : k + 1 ≤ n + 1
⊢ n.choose (k + 1) * (n + 1) = (n + 1).choose (k + 1) * (n + 1 - (k + 1))

Tactic:
rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
  Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem units_eq_one [Subsingleton Mˣ] (u : Mˣ) : u = 1

Proof state:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
u : Mˣ
⊢ u = 1

Tactic:
subsingleton

Result:
no goals
-- Mathlib/CategoryTheory/Shift/CommShift.lean
lemma ofIso_compatibility :
    letI := ofIso e A
    NatTrans.CommShift e.hom A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ NatTrans.CommShift e.hom A

Tactic:
letI := ofIso e A

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
⊢ NatTrans.CommShift e.hom A

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
⊢ NatTrans.CommShift e.hom A

Tactic:
refine ⟨fun a => ?_⟩

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
a : A
⊢ (F.commShiftIso a).hom ≫ whiskerRight e.hom (shiftFunctor D a) =
    whiskerLeft (shiftFunctor C a) e.hom ≫ (G.commShiftIso a).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
a : A
⊢ (iso a).hom ≫ whiskerRight e.hom (shiftFunctor D a) =
    whiskerLeft (shiftFunctor C a) e.hom ≫
      whiskerLeft (shiftFunctor C a) e.inv ≫ (iso a).hom ≫ whiskerRight e.hom (shiftFunctor D a)

Tactic:
rw [← whiskerLeft_comp_assoc, e.hom_inv_id, whiskerLeft_id', id_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
a : A
⊢ (F.commShiftIso a).hom ≫ whiskerRight e.hom (shiftFunctor D a) =
    whiskerLeft (shiftFunctor C a) e.hom ≫ (G.commShiftIso a).hom

Tactic:
dsimp [commShiftIso, ofIso]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Category.{u_6, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
this : G.CommShift A := ofIso e A
a : A
⊢ (iso a).hom ≫ whiskerRight e.hom (shiftFunctor D a) =
    whiskerLeft (shiftFunctor C a) e.hom ≫
      whiskerLeft (shiftFunctor C a) e.inv ≫ (iso a).hom ≫ whiskerRight e.hom (shiftFunctor D a)
-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_think_right (R : α → β → Prop) (s t) : LiftRel R s (think t) ↔ LiftRel R s t

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ LiftRel R s t.think ↔ LiftRel R s t

Tactic:
rw [liftRel_destruct_iff, liftRel_destruct_iff]

Result:
α : Type u
β : Type v
R : α → β → Prop
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.think.destruct ↔
    Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
-- Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean
lemma Hom.toBialgHom_injective (V W : HopfAlgebraCat.{v} R) :
    Function.Injective (Hom.toBialgHom : Hom V W → _) :=
  fun ⟨f⟩ ⟨g⟩ _ => by congr

Proof state:
R : Type u
inst✝ : CommRing R
V W : HopfAlgebraCat R
x✝² x✝¹ : V.Hom W
f g : V.carrier →ₐc[R] W.carrier
x✝ : { toBialgHom' := f }.toBialgHom = { toBialgHom' := g }.toBialgHom
⊢ { toBialgHom' := f } = { toBialgHom' := g }

Tactic:
congr

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem length_pos_of_head_eq_head_of_last_eq_last_of_length_pos {s₁ s₂ : CompositionSeries X}
    (hb : s₁.head = s₂.head) (ht : s₁.last = s₂.last) : 0 < s₁.length → 0 < s₂.length :=
  not_imp_not.1
    (by
      simpa only [pos_iff_ne_zero, ne_eq, Decidable.not_not] using
        length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb.symm ht.symm)

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
⊢ ¬0 < s₂.length → ¬0 < s₁.length

Tactic:
simpa only [pos_iff_ne_zero, ne_eq, Decidable.not_not] using
  length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero hb.symm ht.symm

Result:
no goals
-- Mathlib/Algebra/Category/MonCat/Basic.lean
@[to_additive]
lemma id_apply (M : CommMonCat) (x : M) :
    (𝟙 M : M ⟶ M) x = x

Proof state:
M : CommMonCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/SeparatedMap.lean
lemma isSeparatedMap_iff_disjoint_nhds {f : X → Y} : IsSeparatedMap f ↔
    ∀ x₁ x₂, f x₁ = f x₂ → x₁ ≠ x₂ → Disjoint (𝓝 x₁) (𝓝 x₂) :=
  forall₃_congr fun x x' _ ↦ by simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens x'),
    exists_prop, ← exists_and_left, and_assoc, and_comm, and_left_comm]

Proof state:
X : Type u_1
Y : Sort u_2
inst✝ : TopologicalSpace X
f : X → Y
x x' : X
x✝ : f x = f x'
⊢ (x ≠ x' → ∃ s₁ s₂, IsOpen s₁ ∧ IsOpen s₂ ∧ x ∈ s₁ ∧ x' ∈ s₂ ∧ Disjoint s₁ s₂) ↔ x ≠ x' → Disjoint (𝓝 x) (𝓝 x')

Tactic:
simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens x'),
exists_prop, ← exists_and_left, and_assoc, and_comm, and_left_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty C] :
    Initial F ↔ ∀ d, IsCofiltered (CostructuredArrow F d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
rw [initial_iff_of_isCofiltered]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ ((∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s') →
    ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ F.Initial ↔ ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow F⟩

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
⊢ ((∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s') →
    ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
exact fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addZ_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) : W.addZ P Q = (P x * Q z - Q x * P z) ^ 3 / (P z * Q z)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.addZ P Q = (P x * Q z - Q x * P z) ^ 3 / (P z * Q z)

Tactic:
rw [← addZ_eq' hP hQ, mul_div_cancel_right₀ _ <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
    ¬a ∈ m → m.getKey! a = default

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
a : α
⊢ ¬a ∈ m → m.getKey! a = default

Tactic:
simpa [mem_iff_contains] using getKey!_eq_default_of_contains_eq_false

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Euclidean.lean
theorem abs_isEuclidean : IsEuclidean (AbsoluteValue.abs : AbsoluteValue ℤ ℤ) :=
  {  map_lt_map_iff' := fun {x y} =>
       show abs x < abs y ↔ natAbs x < natAbs y by rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt] }

Proof state:
x y : ℤ
⊢ |x| < |y| ↔ x.natAbs < y.natAbs

Tactic:
rw [abs_eq_natAbs, abs_eq_natAbs, ofNat_lt]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem left_distrib (x y z : X q) : x * (y + z) = x * y + x * z

Proof state:
q : ℕ+
x y z : X q
⊢ x * (y + z) = x * y + x * z

Tactic:
ext <;> dsimp <;> ring

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_closure₂ : hausdorffEdist s (closure t) = hausdorffEdist s t

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
⊢ hausdorffEdist s (closure t) = hausdorffEdist s t

Tactic:
simp [@hausdorffEdist_comm _ _ s _]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblX_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
    W.dblX P / W.dblZ P ^ 2 = W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.dblX P / W.dblZ P ^ 2 =
    (toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
rw [dblX, toAffine_slope_of_eq hP hQ hPz hQz hx hy, dblZ, ← (X_eq_iff hPz hQz).mp hx,
  toAffine_addX_of_eq hPz <| sub_ne_zero.mpr <| Y_ne_negY_of_Y_ne' hP hQ hx hy]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
lemma mFourier_neg : mFourier (-n) x = conj (mFourier n x)

Proof state:
d : Type u_1
inst✝ : Fintype d
n : d → ℤ
x : UnitAddTorus d
⊢ (mFourier (-n)) x = (starRingEnd ℂ) ((mFourier n) x)

Tactic:
simp only [mFourier, Pi.neg_apply, fourier_neg, ContinuousMap.coe_mk, map_prod]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_union' (h : Disjoint s t) (hs : MeasurableSet s) :
    μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
hs : MeasurableSet s
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t

Tactic:
rw [union_comm, restrict_union h.symm hs, add_comm]

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem empty_union (s : Finset α) : ∅ ∪ s = s :=
  ext fun x => mem_union.trans <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ ∅ ∨ x ∈ s ↔ x ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsLowerSet.memberSubfamily (h : IsLowerSet (𝒜 : Set (Finset α))) :
    IsLowerSet (𝒜.memberSubfamily a : Set (Finset α))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
⊢ IsLowerSet ↑(Finset.memberSubfamily a 𝒜)

Tactic:
rintro s t hts

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ ↑(Finset.memberSubfamily a 𝒜) → t ∈ ↑(Finset.memberSubfamily a 𝒜)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t

Tactic:
exact And.imp (h <| insert_subset_insert _ hts) (mt <| @hts _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ s ∈ ↑(Finset.memberSubfamily a 𝒜) → t ∈ ↑(Finset.memberSubfamily a 𝒜)

Tactic:
simp_rw [mem_coe, mem_memberSubfamily]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s t : Finset α
hts : t ≤ s
⊢ insert a s ∈ 𝒜 ∧ a ∉ s → insert a t ∈ 𝒜 ∧ a ∉ t
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_inter_Iio : Ioo a b ∩ Iio c = Ioo a (min b c)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ Ioo a b ∩ Iio c = Ioo a (b ⊓ c)

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c x✝ : α
⊢ x✝ ∈ Ioo a b ∩ Iio c ↔ x✝ ∈ Ioo a (b ⊓ c)

Proof state:
case h
α : Type u_1
inst✝ : LinearOrder α
a b c x✝ : α
⊢ x✝ ∈ Ioo a b ∩ Iio c ↔ x✝ ∈ Ioo a (b ⊓ c)

Tactic:
simp_rw [mem_inter_iff, mem_Ioo, mem_Iio, lt_min_iff, and_assoc]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lsub_lt_ord_lift {ι} {f : ι → Ordinal} {c : Ordinal}
    (hι : Cardinal.lift.{v, u} #ι < c.cof)
    (hf : ∀ i, f i < c) : lsub.{u, v} f < c :=
  lt_of_le_of_ne (lsub_le hf) fun h => by
    subst h
    exact (cof_lsub_le_lift.{u, v} f).not_lt hι

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
c : Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < c.cof
hf : ∀ (i : ι), f i < c
h : lsub f = c
⊢ False

Tactic:
subst h

Result:
ι : Type u
f : ι → Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < (lsub f).cof
hf : ∀ (i : ι), f i < lsub f
⊢ False

Proof state:
ι : Type u
f : ι → Ordinal.{max u v}
hι : Cardinal.lift.{v, u} #ι < (lsub f).cof
hf : ∀ (i : ι), f i < lsub f
⊢ False

Tactic:
exact (cof_lsub_le_lift.{u, v} f).not_lt hι

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem IsProj.trace {p : Submodule R M} {f : M →ₗ[R] M} (h : IsProj p f) [Module.Free R p]
    [Module.Finite R p] [Module.Free R (ker f)] [Module.Finite R (ker f)] :
    trace R M f = (finrank R p : R)

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥(ker f)
inst✝ : Module.Finite R ↥(ker f)
⊢ (LinearMap.trace R M) f = ↑(finrank R ↥p)

Tactic:
rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem definable_empty : A.Definable L (∅ : Set (α → M)) :=
  ⟨⊥, by
    ext
    simp⟩

Proof state:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ setOf ⊥.Realize

Tactic:
simp

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
⊢ ∅ = setOf ⊥.Realize

Tactic:
ext

Result:
case h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
x✝ : α → M
⊢ x✝ ∈ ∅ ↔ x✝ ∈ setOf ⊥.Realize
-- Mathlib/CategoryTheory/Closed/Functor.lean
theorem frobeniusMorphism_iso_of_expComparison_iso (h : L ⊣ F) (A : C)
    [i : IsIso (expComparison F A).natTrans] : IsIso (frobeniusMorphism F h A).natTrans

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i : IsIso (expComparison F A).natTrans
⊢ IsIso (frobeniusMorphism F h A).natTrans

Tactic:
rw [← frobeniusMorphism_mate F h] at i

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso
    ((conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)
⊢ IsIso (frobeniusMorphism F h A).natTrans

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : ChosenFiniteProducts D
F : C ⥤ D
L : D ⥤ C
inst✝² : CartesianClosed C
inst✝¹ : CartesianClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
h : L ⊣ F
A : C
i :
  IsIso
    ((conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h))
      (frobeniusMorphism F h A).natTrans)
⊢ IsIso (frobeniusMorphism F h A).natTrans

Tactic:
exact @conjugateEquiv_of_iso _ _ _ _ _ _ _ _ _ _ _ i

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_eq_head_iff_eq_getLast (x y : α) :
    formPerm (y :: l) x = y ↔ x = getLast (y :: l) (cons_ne_nil _ _) :=
  Iff.trans (by rw [formPerm_apply_getLast]) (formPerm (y :: l)).injective.eq_iff

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
⊢ (y :: l).formPerm x = y ↔ (y :: l).formPerm x = (y :: l).formPerm ((y :: l).getLast ⋯)

Tactic:
rw [formPerm_apply_getLast]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem Pairwise.imp_mem {l : List α} :
    Pairwise R l ↔ Pairwise (fun x y => x ∈ l → y ∈ l → R x y) l :=
  Pairwise.iff_of_mem <| by simp +contextual

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
⊢ ∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ a ∈ l → b ∈ l → R a b)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_ofList_of_contains_eq_false [LawfulBEq α]
    {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (ofList l).get! k = default

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k : α
inst✝ : Inhabited (β k)
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (ofList l).get! k = default

Tactic:
simp_to_raw using get!_insertMany_empty_list_of_contains_eq_false

Result:
no goals