harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q)
    (hQz : Q z = 0) : W'.negAddY P Q = -(Q y ^ 2 * P z) * W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.negAddY P Q = -(Q y ^ 2 * P z) * W'.negY P

Tactic:
rw [negAddY, hQz, X_eq_zero_of_Z_eq_zero hQ hQz, negY]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
ring1

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem extraction_of_frequently_atTop {P : ℕ → Prop} (h : ∃ᶠ n in atTop, P n) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∀ n, P (φ n)

Proof state:
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
exact extraction_of_frequently_atTop' h

Result:
no goals

Proof state:
P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
rw [frequently_atTop'] at h

Result:
P : ℕ → Prop
h : ∀ (a : ℕ), ∃ b > a, P b
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem HasProd.hasProd_iff_compl {s : Set β} (hf : HasProd (f ∘ (↑) : s → α) a₁) :
    HasProd f a₂ ↔ HasProd (f ∘ (↑) : ↑sᶜ → α) (a₂ / a₁) :=
  Iff.symm <| hf.hasProd_compl_iff.trans <| by rw [mul_div_cancel]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f : β → α
a₁ a₂ : α
s : Set β
hf : HasProd (f ∘ Subtype.val) a₁
⊢ HasProd f (a₁ * (a₂ / a₁)) ↔ HasProd f a₂

Tactic:
rw [mul_div_cancel]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem subtypeVal_toSubtype' {α : TypeVec n} (r : α ⊗ α ⟹ «repeat» n Prop) :
    subtypeVal r ⊚ toSubtype' r = fun i x => prod.mk i x.1.fst x.1.snd

Proof state:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.1 x.2)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).1 (↑x).2

Tactic:
simp [*]

Result:
no goals

Proof state:
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
⊢ subtypeVal r ⊚ toSubtype' r = fun i x => prod.mk i (↑x).1 (↑x).2

Tactic:
ext i x

Result:
case a.h
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (r i (prod.mk i x.1 x.2)) }) i
⊢ (subtypeVal r ⊚ toSubtype' r) i x = prod.mk i (↑x).1 (↑x).2

Proof state:
case a.h
n : ℕ
α : TypeVec.{u_1} n
r : α ⊗ α ⟹ «repeat» n Prop
i : Fin2 n
x : (fun i => { x // ofRepeat (r i (prod.mk i x.1 x.2)) }) i
⊢ (subtypeVal r ⊚ toSubtype' r) i x = prod.mk i (↑x).1 (↑x).2

Tactic:
induction i <;> simp only [id, toSubtype', comp, subtypeVal, prod.mk] at *

Result:
case a.h.fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (r : α ⊗ α ⟹ «repeat» n✝ Prop) (x : { x // ofRepeat (r a✝ (prod.mk a✝ x.1 x.2)) }),
    subtypeVal r a✝ (toSubtype' r a✝ x) = prod.mk a✝ (↑x).1 (↑x).2
α : TypeVec.{u_1} (n✝ + 1)
r : α ⊗ α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (r a✝.fs (prod.mk a✝.fs x.1 x.2)) }
⊢ subtypeVal (dropFun r) a✝ (toSubtype' (dropFun r) a✝ x) = prod.mk a✝ (↑x).1 (↑x).2
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inr_fst_assoc {K : CochainComplex C ℤ} {d e f : ℤ} (γ : Cochain F K d)
    (he : 1 + d = e) (hf : 0 + e = f) :
    (Cochain.ofHom (inr φ)).comp ((fst φ).1.comp γ he) hf = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e f : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = f
⊢ e = f

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e f : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = f
⊢ (Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0

Tactic:
obtain rfl : e = f := by omega

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
⊢ (Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
⊢ (Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0

Tactic:
rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_fst, Cochain.zero_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_tail : ∀ (l : List α) (a : α) (h : l ≠ []),
      l.tail.count a = l.count a - if l.head h == a then 1 else 0
  | head :: tail, a, _ => by simp [count_cons]

Proof state:
α : Type u_1
inst✝ : BEq α
head : α
tail : List α
a : α
x✝ : head :: tail ≠ []
⊢ count a (head :: tail).tail = count a (head :: tail) - if ((head :: tail).head x✝ == a) = true then 1 else 0

Tactic:
simp [count_cons]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem lipschitzWith_one_mulExpNegMulSq (hε : 0 < ε) :
    LipschitzWith 1 (mulExpNegMulSq ε)

Proof state:
ε : ℝ
hε : 0 < ε
⊢ LipschitzWith 1 ε.mulExpNegMulSq

Tactic:
apply lipschitzWith_of_nnnorm_deriv_le differentiable_mulExpNegMulSq

Result:
ε : ℝ
hε : 0 < ε
⊢ ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
⊢ ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Tactic:
exact nnnorm_deriv_mulExpNegMulSq_le_one hε

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem Prop.exists_iff {p : Prop → Prop} : (∃ h, p h) ↔ p False ∨ p True :=
  ⟨fun ⟨h₁, h₂⟩ ↦ by_cases (fun H : h₁ ↦ .inr <| by simpa only [H] using h₂)
    (fun H ↦ .inl <| by simpa only [H] using h₂), fun h ↦ h.elim (.intro _) (.intro _)⟩

Proof state:
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False

Tactic:
simpa only [H] using h₂

Result:
no goals

Proof state:
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True

Tactic:
simpa only [H] using h₂

Result:
no goals
-- Mathlib/RingTheory/Flat/Equalizer.lean
lemma Module.Flat.ker_lTensor_eq [Module.Flat R M] :
    LinearMap.ker (AlgebraTensorModule.lTensor S M f) =
      LinearMap.range (AlgebraTensorModule.lTensor S M (LinearMap.ker f).subtype)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Flat R M
⊢ LinearMap.ker ((AlgebraTensorModule.lTensor S M) f) =
    LinearMap.range ((AlgebraTensorModule.lTensor S M) (LinearMap.ker f).subtype)

Tactic:
rw [← LinearMap.exact_iff]

Result:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Flat R M
⊢ Function.Exact ⇑((AlgebraTensorModule.lTensor S M) (LinearMap.ker f).subtype) ⇑((AlgebraTensorModule.lTensor S M) f)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
M : Type u_3
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : IsScalarTower R S M
N : Type u_4
P : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R N
inst✝¹ : Module R P
f : N →ₗ[R] P
inst✝ : Flat R M
⊢ Function.Exact ⇑((AlgebraTensorModule.lTensor S M) (LinearMap.ker f).subtype) ⇑((AlgebraTensorModule.lTensor S M) f)

Tactic:
exact Module.Flat.lTensor_exact M (LinearMap.exact_subtype_ker_map f)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.ι_π_ne (f : J → C) [HasBiproduct f] {j j' : J} (h : j ≠ j') :
    biproduct.ι f j ≫ biproduct.π f j' = 0

Proof state:
J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j j' : J
h : j ≠ j'
⊢ ι f j ≫ π f j' = 0

Tactic:
simp [biproduct.ι_π, h]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
theorem IsOpen.exists_subset_affineIndependent_span_eq_top {u : Set P} (hu : IsOpen u)
    (hne : u.Nonempty) : ∃ s ⊆ u, AffineIndependent ℝ ((↑) : s → P) ∧ affineSpan ℝ s = ⊤

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
hne : u.Nonempty
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤

Tactic:
rcases hne with ⟨x, hx⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤

Proof state:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
s : Set P
hsu : s ⊆ u
hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤

Tactic:
exact ⟨s, hsu, hs⟩

Result:
no goals

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤

Tactic:
rcases hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx)
  (singleton_nonempty _) (affineIndependent_of_subsingleton _ _) with ⟨s, -, hsu, hs⟩

Result:
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
s : Set P
hsu : s ⊆ u
hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) :
    (n + 1).ascFactorial k = k ! * (n + k).choose k

Proof state:
n k : ℕ
⊢ (n + 1).ascFactorial k = k ! * (n + k).choose k

Tactic:
rw [Nat.mul_comm]

Result:
n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !

Proof state:
n k : ℕ
⊢ (n + 1).ascFactorial k = (n + k).choose k * k !

Tactic:
apply Nat.mul_right_cancel (n + k - k).factorial_pos

Result:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!

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

Tactic:
rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
  ← factorial_mul_ascFactorial, Nat.mul_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_b₄ :
    (W.variableChange C).b₄ = C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 2 * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
      ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
    ↑C.u⁻¹ ^ 4 * (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (W.a₁ ^ 2 + 4 * W.a₂) + 6 * C.r ^ 2)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (W.variableChange C).b₄ = ↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)

Tactic:
simp only [b₂, b₄, variableChange_a₁, variableChange_a₃, variableChange_a₄]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ 2 * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) +
      ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) =
    ↑C.u⁻¹ ^ 4 * (2 * W.a₄ + W.a₁ * W.a₃ + C.r * (W.a₁ ^ 2 + 4 * W.a₂) + 6 * C.r ^ 2)
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_neg (x y : ℂ) : x ^ (-y) = (x ^ y)⁻¹

Proof state:
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (-(log x * y))) =
    (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y))⁻¹

Tactic:
split_ifs <;> simp [exp_neg]

Result:
no goals

Proof state:
x y : ℂ
⊢ x ^ (-y) = (x ^ y)⁻¹

Tactic:
simp only [cpow_def, neg_eq_zero, mul_neg]

Result:
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (-(log x * y))) =
    (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y))⁻¹
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_ofNat (n : Nat) [n.AtLeastTwo] :
    withTopEquiv.symm ofNat(n) = OfNat.ofNat n

Proof state:
n : ℕ
inst✝ : n.AtLeastTwo
⊢ withTopEquiv.symm (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_concat (i : B) (ω : List B) : π (ω.concat i) = π ω * s i

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
⊢ cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i

Tactic:
simp [wordProd]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mkHom_f_succ_succ (n : ℕ) :
    (mkHom P Q zero one one_zero_comm succ).f (n + 2) =
      (succ n
          ⟨(mkHom P Q zero one one_zero_comm succ).f n,
            (mkHom P Q zero one one_zero_comm succ).f (n + 1),
            (mkHom P Q zero one one_zero_comm succ).comm (n + 1) n⟩).1

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst

Tactic:
dsimp [mkHom, mkHomAux]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma adj_snd {p : G.Walk v w} (hp : ¬ p.Nil) :
    G.Adj v p.snd

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ G.Adj v p.snd

Tactic:
simpa using adj_getVert_succ p (by simpa [not_nil_iff_lt_length] using hp : 0 < p.length)

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
p : G.Walk v w
hp : ¬p.Nil
⊢ 0 < p.length

Tactic:
simpa [not_nil_iff_lt_length] using hp

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
theorem Matrix.toLin_kronecker (A : Matrix ι' ι R) (B : Matrix κ' κ R) :
    toLin (bM.tensorProduct bN) (bM'.tensorProduct bN') (A ⊗ₖ B) =
      TensorProduct.map (toLin bM bM' A) (toLin bN bN' B)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
M' : Type u_5
N' : Type u_6
ι : Type u_7
κ : Type u_8
ι' : Type u_10
κ' : Type u_11
inst✝¹⁴ : DecidableEq ι
inst✝¹³ : DecidableEq κ
inst✝¹² : Fintype ι
inst✝¹¹ : Fintype κ
inst✝¹⁰ : Finite ι'
inst✝⁹ : Finite κ'
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup M'
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R M'
inst✝ : Module R N'
bM : Basis ι R M
bN : Basis κ R N
bM' : Basis ι' R M'
bN' : Basis κ' R N'
A : Matrix ι' ι R
B : Matrix κ' κ R
⊢ (toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (kroneckerMap (fun x1 x2 => x1 * x2) A B) =
    TensorProduct.map ((toLin bM bM') A) ((toLin bN bN') B)

Tactic:
rw [← LinearEquiv.eq_symm_apply, toLin_symm, TensorProduct.toMatrix_map, toMatrix_toLin,
  toMatrix_toLin]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_self : e.det e = 1

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
⊢ e.det ⇑e = 1

Tactic:
simp [e.det_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negAddY_eq {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) : W.negAddY P Q =
    ((P y * Q z ^ 3 - Q y * P z ^ 3) * (W.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2)
      + P y * Q z ^ 3 * addZ P Q ^ 3) / (P z * Q z) ^ 3

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
⊢ W.negAddY P Q =
    ((P y * Q z ^ 3 - Q y * P z ^ 3) * (W.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2) +
        P y * Q z ^ 3 * addZ P Q ^ 3) /
      (P z * Q z) ^ 3

Tactic:
rw [← negAddY_eq', mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
    (pj : j < (a.set i v).size) (h : i ≠ j) :
    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj)

Proof state:
α : Type u_1
a : Array α
i : Nat
h' : i < a.size
v : α
j : Nat
pj : j < (a.set i v h').size
h : i ≠ j
⊢ (a.set i v h')[j] = a[j]

Tactic:
simp only [set, ← getElem_toList, List.getElem_set_ne h]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Center.lean
@[simp] lemma zero_mem_centralizer : (0 : M₀) ∈ centralizer s

Proof state:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
s : Set M₀
⊢ 0 ∈ s.centralizer

Tactic:
simp [mem_centralizer_iff]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem mul_fin_two [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
    !![a₁₁, a₁₂;
       a₂₁, a₂₂] * !![b₁₁, b₁₂;
                      b₂₁, b₂₂] = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂;
                                     a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]

Proof state:
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
⊢ !![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂] =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂]

Tactic:
ext i j

Result:
case a
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j

Proof state:
case a
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j

Tactic:
fin_cases i <;> fin_cases j <;> simp [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem dist_div_sin_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P}
    (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) : dist p₃ p₂ / Real.Angle.sin (∡ p₃ p₁ p₂) = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ dist p₃ p₂ / (∡ p₃ p₁ p₂).sin = dist p₁ p₃

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.sin_coe, dist_comm p₁ p₃,
  dist_div_sin_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)
    (Or.inl (right_ne_of_oangle_eq_pi_div_two h))]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
theorem not_mem_iff_exists_ne_and_isConjRoot {x : L} (h : IsSeparable K x)
    (sp : (minpoly K x).Splits (algebraMap K L)) :
    x ∉ (⊥ : Subalgebra K L) ↔ ∃ y : L, x ≠ y ∧ IsConjRoot K x y

Proof state:
K : Type u_2
L : Type u_3
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : IsSeparable K x
sp : Splits (algebraMap K L) (minpoly K x)
⊢ x ∉ ⊥ ↔ ∃ y, x ≠ y ∧ IsConjRoot K x y

Tactic:
calc
  _ ↔ 2 ≤ (minpoly K x).natDegree := (minpoly.two_le_natDegree_iff h.isIntegral).symm
  _ ↔ 2 ≤ Fintype.card ((minpoly K x).rootSet L) :=
    (Polynomial.card_rootSet_eq_natDegree h sp) ▸ Iff.rfl
  _ ↔ Nontrivial ((minpoly K x).rootSet L) := Fintype.one_lt_card_iff_nontrivial
  _ ↔ ∃ y : ((minpoly K x).rootSet L), ↑y ≠ x :=
    (nontrivial_iff_exists_ne ⟨x, mem_rootSet.mpr ⟨minpoly.ne_zero h.isIntegral,
        minpoly.aeval K x⟩⟩).trans ⟨fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mpr hy⟩,
        fun ⟨y, hy⟩ => ⟨y, Subtype.coe_ne_coe.mp hy⟩⟩
  _ ↔ _ :=
    ⟨fun ⟨⟨y, hy⟩, hne⟩ => ⟨y, ⟨hne.symm,
        (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mpr hy⟩⟩,
        fun ⟨y, hne, hy⟩ => ⟨⟨y,
        (isConjRoot_iff_mem_minpoly_rootSet h.isIntegral).mp hy⟩, hne.symm⟩⟩

Result:
no goals