harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
lemma posSemidef_sqrt : PosSemidef hA.sqrt

Proof state:
case hA
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) i

Tactic:
rw [Function.comp_apply, RCLike.nonneg_iff]

Result:
case hA
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ RCLike.re ↑((Real.sqrt ∘ ⋯.eigenvalues) i) ∧ RCLike.im ↑((Real.sqrt ∘ ⋯.eigenvalues) i) = 0

Proof state:
case hA
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)).PosSemidef

Tactic:
refine posSemidef_diagonal_iff.mpr fun i ↦ ?_

Result:
case hA
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues) i

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ hA.sqrt.PosSemidef

Tactic:
apply PosSemidef.mul_mul_conjTranspose_same

Result:
case hA
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
⊢ (diagonal (RCLike.ofReal ∘ Real.sqrt ∘ ⋯.eigenvalues)).PosSemidef

Proof state:
case hA
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ RCLike.re ↑((Real.sqrt ∘ ⋯.eigenvalues) i) ∧ RCLike.im ↑((Real.sqrt ∘ ⋯.eigenvalues) i) = 0

Tactic:
constructor

Result:
case hA.left
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ RCLike.re ↑((Real.sqrt ∘ ⋯.eigenvalues) i)

case hA.right
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ RCLike.im ↑((Real.sqrt ∘ ⋯.eigenvalues) i) = 0

Proof state:
case hA.left
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ (Real.sqrt ∘ ⋯.eigenvalues) i

Tactic:
exact Real.sqrt_nonneg _

Result:
no goals

Proof state:
case hA.right
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ RCLike.im ↑((Real.sqrt ∘ ⋯.eigenvalues) i) = 0

Tactic:
simp only [RCLike.ofReal_im]

Result:
no goals

Proof state:
case hA.left
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ RCLike.re ↑((Real.sqrt ∘ ⋯.eigenvalues) i)

Tactic:
simp only [RCLike.ofReal_re]

Result:
case hA.left
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
i : n
⊢ 0 ≤ (Real.sqrt ∘ ⋯.eigenvalues) i
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.Unsat

Proof state:
case mp
entry : Entrypoint Nat
h :
  CNF.Unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ ⟦assign1, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = false

Tactic:
apply toCNF.go_as_denote

Result:
case mp.a
entry : Entrypoint Nat
h :
  CNF.Unsat
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
assign1 : Nat → Bool
⊢ (⟦assign1, { aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ &&
      toCNF.State.eval (toCNF.cnfSatAssignment entry.aig assign1)
        (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val) =
    false

Proof state:
case a
entry : Entrypoint Nat
a b : entry.aig.CNFVar
a✝¹ :
  CNF.Mem a
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
a✝ :
  CNF.Mem b
    ([(Sum.inr ⟨entry.ref.gate, ⋯⟩, true)] ::
      (toCNF.go entry.aig entry.ref.gate ⋯ (toCNF.State.empty entry.aig)).val.cnf)
hinj : toCNF.inj a = toCNF.inj b
⊢ toCNF.inj a = toCNF.inj b

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.isBase_of_isBasis_superset (hB : M.IsBase B) (hBX : B ⊆ X) (hIX : M.IsBasis I X) :
    M.IsBase I

Proof state:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
⊢ False

Tactic:
obtain ⟨e,heBI,he⟩ := hIX.indep.exists_insert_of_not_isBase h hB

Result:
case intro.intro
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
e : α
heBI : e ∈ B \ I
he : M.Indep (insert e I)
⊢ False

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
e : α
heBI : e ∈ B \ I
he : M.Indep (insert e I)
⊢ False

Tactic:
exact heBI.2 (hIX.mem_of_insert_indep (hBX heBI.1) he)

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
⊢ M.IsBase I

Tactic:
by_contra h

Result:
α : Type u_1
M : Matroid α
B I X : Set α
hB : M.IsBase B
hBX : B ⊆ X
hIX : M.IsBasis I X
h : ¬M.IsBase I
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) :
    m.size - 1 ≤ (Const.alter m k f).size

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
k : α
f : Option β → Option β
h : m.WF
⊢ m.size - 1 ≤ (alter m k f).size

Tactic:
simp_to_raw using Raw₀.Const.size_le_size_alter ⟨m, h.size_buckets_pos⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_isSome {xs : List α} {p : α → Bool} : (xs.find? p).isSome ↔ ∃ x, x ∈ xs ∧ p x

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ (find? p xs).isSome = true ↔ ∃ x, x ∈ xs ∧ p x = true

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp only [find?_cons, mem_cons, exists_eq_or_imp]
  split <;> simp_all

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (find? p xs).isSome = true ↔ ∃ x, x ∈ xs ∧ p x = true
⊢ (find? p (x :: xs)).isSome = true ↔ ∃ x_1, x_1 ∈ x :: xs ∧ p x_1 = true

Tactic:
simp only [find?_cons, mem_cons, exists_eq_or_imp]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (find? p xs).isSome = true ↔ ∃ x, x ∈ xs ∧ p x = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).isSome =
      true ↔
    p x = true ∨ ∃ a, a ∈ xs ∧ p a = true

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ (find? p []).isSome = true ↔ ∃ x, x ∈ [] ∧ p x = true

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : (find? p xs).isSome = true ↔ ∃ x, x ∈ xs ∧ p x = true
⊢ (match p x with
        | true => some x
        | false => find? p xs).isSome =
      true ↔
    p x = true ∨ ∃ a, a ∈ xs ∧ p a = true

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma prod_Iio_mul_eq_prod_Iic (a : α) : (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
inst✝ : LocallyFiniteOrderBot α
a : α
⊢ (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Tactic:
rw [mul_comm, mul_prod_Iio_eq_prod_Iic]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem prodIsoProd_hom_apply {X Y : TopCat.{u}} (x : ↑(X ⨯ Y)) :
    (prodIsoProd X Y).hom x = ((Limits.prod.fst : X ⨯ Y ⟶ _) x,
    (Limits.prod.snd : X ⨯ Y ⟶ _) x)

Proof state:
case fst
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((ConcreteCategory.hom (X.prodIsoProd Y).hom) x).1 =
    ((ConcreteCategory.hom prod.fst) x, (ConcreteCategory.hom prod.snd) x).1

Tactic:
exact ConcreteCategory.congr_hom (prodIsoProd_hom_fst X Y) x

Result:
no goals

Proof state:
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ (ConcreteCategory.hom (X.prodIsoProd Y).hom) x =
    ((ConcreteCategory.hom prod.fst) x, (ConcreteCategory.hom prod.snd) x)

Tactic:
ext

Result:
case fst
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((ConcreteCategory.hom (X.prodIsoProd Y).hom) x).1 =
    ((ConcreteCategory.hom prod.fst) x, (ConcreteCategory.hom prod.snd) x).1

case snd
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((ConcreteCategory.hom (X.prodIsoProd Y).hom) x).2 =
    ((ConcreteCategory.hom prod.fst) x, (ConcreteCategory.hom prod.snd) x).2

Proof state:
case snd
X Y : TopCat
x : ↑(X ⨯ Y)
⊢ ((ConcreteCategory.hom (X.prodIsoProd Y).hom) x).2 =
    ((ConcreteCategory.hom prod.fst) x, (ConcreteCategory.hom prod.snd) x).2

Tactic:
exact ConcreteCategory.congr_hom (prodIsoProd_hom_snd X Y) x

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma support_eq_empty_iff : support I = ∅ ↔ I = ⊤

Proof state:
X : Scheme
I : X.IdealSheafData
⊢ I = ⊤ → I.support = ∅

Tactic:
simp +contextual

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
H : I.support = ∅
U : ↑X.affineOpens
⊢ ⊤.ideal U ≤ I.ideal U

Tactic:
have := (U.2.fromSpec_image_zeroLocus _).trans_subset
  ((zeroLocus_inter_subset_support I U).trans_eq H)

Result:
X : Scheme
I : X.IdealSheafData
H : I.support = ∅
U : ↑X.affineOpens
this : ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) '' PrimeSpectrum.zeroLocus ↑(I.ideal U) ⊆ ∅
⊢ ⊤.ideal U ≤ I.ideal U

Proof state:
X : Scheme
I : X.IdealSheafData
⊢ I.support = ∅ ↔ I = ⊤

Tactic:
refine ⟨fun H ↦ top_le_iff.mp fun U ↦ ?_, by simp +contextual⟩

Result:
X : Scheme
I : X.IdealSheafData
H : I.support = ∅
U : ↑X.affineOpens
⊢ ⊤.ideal U ≤ I.ideal U

Proof state:
X : Scheme
I : X.IdealSheafData
H : I.support = ∅
U : ↑X.affineOpens
this : PrimeSpectrum.zeroLocus ↑(I.ideal U) = ∅
⊢ ⊤.ideal U ≤ I.ideal U

Tactic:
simp [PrimeSpectrum.zeroLocus_empty_iff_eq_top.mp this]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
H : I.support = ∅
U : ↑X.affineOpens
this : ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) '' PrimeSpectrum.zeroLocus ↑(I.ideal U) ⊆ ∅
⊢ ⊤.ideal U ≤ I.ideal U

Tactic:
simp only [Set.subset_empty_iff, Set.image_eq_empty] at this

Result:
X : Scheme
I : X.IdealSheafData
H : I.support = ∅
U : ↑X.affineOpens
this : PrimeSpectrum.zeroLocus ↑(I.ideal U) = ∅
⊢ ⊤.ideal U ≤ I.ideal U
-- Mathlib/Data/Num/Lemmas.lean
theorem size_to_nat : ∀ n, (size n : ℕ) = Nat.size n
  | 1 => Nat.size_one.symm
  | bit0 n => by
      rw [size, succ_to_nat, size_to_nat n, cast_bit0, ← two_mul]
      erw [@Nat.size_bit false n]
      have := to_nat_pos n
      dsimp [Nat.bit]; omega
  | bit1 n => by
      rw [size, succ_to_nat, size_to_nat n, cast_bit1, ← two_mul]
      erw [@Nat.size_bit true n]
      dsimp [Nat.bit]; omega

Proof state:
n : PosNum
⊢ (↑n).size + 1 = (2 * ↑n).size

Tactic:
erw [@Nat.size_bit false n]

Result:
n : PosNum
⊢ Nat.bit false ↑n ≠ 0

Proof state:
n : PosNum
⊢ Nat.bit false ↑n ≠ 0

Tactic:
have := to_nat_pos n

Result:
n : PosNum
this : 0 < ↑n
⊢ Nat.bit false ↑n ≠ 0

Proof state:
n : PosNum
this : 0 < ↑n
⊢ Nat.bit false ↑n ≠ 0

Tactic:
dsimp [Nat.bit]

Result:
n : PosNum
this : 0 < ↑n
⊢ ¬2 * ↑n = 0

Proof state:
n : PosNum
⊢ ↑n.bit1.size = (↑n.bit1).size

Tactic:
rw [size, succ_to_nat, size_to_nat n, cast_bit1, ← two_mul]

Result:
n : PosNum
⊢ (↑n).size + 1 = (2 * ↑n + 1).size

Proof state:
n : PosNum
⊢ (↑n).size + 1 = (2 * ↑n + 1).size

Tactic:
erw [@Nat.size_bit true n]

Result:
n : PosNum
⊢ Nat.bit true ↑n ≠ 0

Proof state:
n : PosNum
⊢ ¬2 * ↑n + 1 = 0

Tactic:
omega

Result:
no goals

Proof state:
n : PosNum
⊢ ↑n.bit0.size = (↑n.bit0).size

Tactic:
rw [size, succ_to_nat, size_to_nat n, cast_bit0, ← two_mul]

Result:
n : PosNum
⊢ (↑n).size + 1 = (2 * ↑n).size

Proof state:
n : PosNum
this : 0 < ↑n
⊢ ¬2 * ↑n = 0

Tactic:
omega

Result:
no goals

Proof state:
n : PosNum
⊢ Nat.bit true ↑n ≠ 0

Tactic:
dsimp [Nat.bit]

Result:
n : PosNum
⊢ ¬2 * ↑n + 1 = 0
-- Mathlib/Data/Set/Lattice.lean
theorem iInter_iInter_eq_or_left {b : β} {p : β → Prop} {s : ∀ x : β, x = b ∨ p x → Set α} :
    ⋂ (x) (h), s x h = s b (Or.inl rfl) ∩ ⋂ (x) (h : p x), s x (Or.inr h)

Proof state:
α : Type u_1
β : Type u_2
b : β
p : β → Prop
s : (x : β) → x = b ∨ p x → Set α
⊢ ⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯

Tactic:
simp only [iInter_or, iInter_inter_distrib, iInter_iInter_eq_left]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean
/--
if `r` has no zero smul divisors for all small-enough sections, then `r` has no zero smul divisors
in the colimit.
-/
lemma colimit_no_zero_smul_divisor
    (F : J ⥤ ModuleCat.{max t w} R) [PreservesColimit F (forget (ModuleCat R))]
    [IsFiltered J] [HasColimit F]
    (r : R) (H : ∃ (j' : J), ∀ (j : J) (_ : j' ⟶ j), ∀ (c : F.obj j), r • c = 0 → c = 0)
    (x : ToType (colimit F)) (hx : r • x = 0) : x = 0

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
simpa [elementwise_of% (colimit.w F), map_zero] using congr(colimit.ι F _
  $(H (IsFiltered.sup {j, j', j''} { ⟨j, j', by simp, by simp, i⟩ })
    (IsFiltered.toSup _ _ <| by simp)
    (F.map (IsFiltered.toSup _ _ <| by simp) x)
    (by rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp,
      ModuleCat.comp_apply, ← map_smul, ← map_smul, h, map_zero])))

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j'' ∈ {j, j', j''}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/BaseChange.lean
theorem bracket_lie_self (x : A ⊗[R] L) : ⁅x, x⁆ = 0

Proof state:
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) x) x = 0

Tactic:
refine x.induction_on ?_ ?_ ?_

Result:
case refine_1
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) 0) 0 = 0

case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x : A) (y : L), ((LieAlgebra.ExtendScalars.bracket' R A L L) (x ⊗ₜ[R] y)) (x ⊗ₜ[R] y) = 0

case refine_3
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x y : A ⊗[R] L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) x) x = 0 →
      ((LieAlgebra.ExtendScalars.bracket' R A L L) y) y = 0 →
        ((LieAlgebra.ExtendScalars.bracket' R A L L) (x + y)) (x + y) = 0

Proof state:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
⊢ ∀ (x : A) (y : L), ((LieAlgebra.ExtendScalars.bracket' R A L L) (x ⊗ₜ[R] y)) (x ⊗ₜ[R] y) = 0

Tactic:
intro a l

Result:
case refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x : A ⊗[R] L
a : A
l : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (a ⊗ₜ[R] l)) (a ⊗ₜ[R] l) = 0

Proof state:
case refine_3.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
⊢ ∀ (x : A) (y : L),
    ((LieAlgebra.ExtendScalars.bracket' R A L L) (x ⊗ₜ[R] y)) z₂ +
        ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (x ⊗ₜ[R] y) =
      0

Tactic:
intro a₁ l₁

Result:
case refine_3.refine_2
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
x z₁ z₂ : A ⊗[R] L
h₁ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₁) z₁ = 0
h₂ : ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) z₂ = 0
a₁ : A
l₁ : L
⊢ ((LieAlgebra.ExtendScalars.bracket' R A L L) (a₁ ⊗ₜ[R] l₁)) z₂ +
      ((LieAlgebra.ExtendScalars.bracket' R A L L) z₂) (a₁ ⊗ₜ[R] l₁) =
    0
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_induction {s : Set (Set α)} {i : Ordinal} {t : Set α}
    {p : Set α → Prop} (hs : ∀ t ∈ s, p t) (h0 : p ∅)
    (hc : ∀ u, p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ)
    (hn : ∀ f : ℕ → Set α,
      (∀ n, p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)) :
    t ∈ generateMeasurableRec s i → p t

Proof state:
case inl.inr
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t✝ : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
t : Set α
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
ht : ∃ x, (∃ i, ∃ (_ : i < k), x ∈ generateMeasurableRec s i) ∧ xᶜ = t
⊢ p t

Tactic:
obtain ⟨u, ⟨⟨j, hj, hj'⟩, rfl⟩⟩ := ht

Result:
case inl.inr.intro.intro.intro.intro
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k✝ k : Ordinal.{u_1}
hk : k ≤ i
IH : ∀ j < k, ∀ t ∈ generateMeasurableRec s j, p t
u : Set α
j : Ordinal.{u_1}
hj : j < k
hj' : u ∈ generateMeasurableRec s j
⊢ p uᶜ

Proof state:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
⊢ ∀ k ≤ i, ∀ t ∈ generateMeasurableRec s k, p t

Tactic:
intro k

Result:
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
t : Set α
p : Set α → Prop
hs : ∀ t ∈ s, p t
h0 : p ∅
hc : ∀ (u : Set α), p u → (∃ j < i, u ∈ generateMeasurableRec s j) → p uᶜ
hn : ∀ (f : ℕ → Set α), (∀ (n : ℕ), p (f n) ∧ ∃ j < i, f n ∈ generateMeasurableRec s j) → p (⋃ n, f n)
k : Ordinal.{u_1}
⊢ k ≤ i → ∀ t ∈ generateMeasurableRec s k, p t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem array₂_induction (P : Array (Array α) → Prop) (of : ∀ (xss : List (List α)), P (xss.map List.toArray).toArray)
    (ass : Array (Array α)) : P ass

Proof state:
α : Type u_1
P : Array (Array α) → Prop
ass : Array (Array α)
of : P (List.map List.toArray (List.map toList ass.toList)).toArray
⊢ P ass

Tactic:
simpa [← toList_map, Function.comp_def, map_id] using of

Result:
no goals

Proof state:
α : Type u_1
P : Array (Array α) → Prop
of : ∀ (xss : List (List α)), P (List.map List.toArray xss).toArray
ass : Array (Array α)
⊢ P ass

Tactic:
specialize of (ass.toList.map toList)

Result:
α : Type u_1
P : Array (Array α) → Prop
ass : Array (Array α)
of : P (List.map List.toArray (List.map toList ass.toList)).toArray
⊢ P ass
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
@[simp] lemma coe_nonZeroDivisorsLeft_eq [NoZeroDivisors M₀] [Nontrivial M₀] :
    nonZeroDivisorsLeft M₀ = {x : M₀ | x ≠ 0}

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (a : M₀), x = 0 → a = 0
⊢ x ≠ 0

Tactic:
contrapose! h

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ a, x = 0 ∧ a ≠ 0

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}

Tactic:
simp only [SetLike.mem_coe, mem_nonZeroDivisorsLeft_iff, mul_eq_zero, forall_eq_or_imp, true_and,
  Set.mem_setOf_eq]

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ (∀ (a : M₀), x = 0 → a = 0) ↔ x ≠ 0

Tactic:
refine ⟨fun h ↦ ?_, fun hx y hx' ↦ by contradiction⟩

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : ∀ (a : M₀), x = 0 → a = 0
⊢ x ≠ 0

Proof state:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ a, x = 0 ∧ a ≠ 0

Tactic:
exact ⟨1, h, one_ne_zero⟩

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
⊢ ↑(nonZeroDivisorsLeft M₀) = {x | x ≠ 0}

Tactic:
ext x

Result:
case h
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
⊢ x ∈ ↑(nonZeroDivisorsLeft M₀) ↔ x ∈ {x | x ≠ 0}

Proof state:
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0
⊢ y = 0

Tactic:
contradiction

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_of_Z_eq_zero_left {P Q : Fin 3 → R} (hPz : P z = 0) :
    W'.addX P Q = (P x * Q z) ^ 2 * Q x

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hPz : P z = 0
⊢ W'.addX P Q = (P x * Q z) ^ 2 * Q x

Tactic:
rw [addX, hPz]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q x ^ 2 * 0 ^ 2 - 2 * P y * Q y * 0 * Q z + P x ^ 2 * Q x * Q z ^ 2 - W'.a₁ * P x * Q y * 0 ^ 2 * Q z -
                  W'.a₁ * P y * Q x * 0 * Q z ^ 2 +
                2 * W'.a₂ * P x * Q x * 0 ^ 2 * Q z ^ 2 -
              W'.a₃ * Q y * 0 ^ 4 * Q z -
            W'.a₃ * P y * 0 * Q z ^ 4 +
          W'.a₄ * Q x * 0 ^ 4 * Q z ^ 2 +
        W'.a₄ * P x * 0 ^ 2 * Q z ^ 4 +
      2 * W'.a₆ * 0 ^ 4 * Q z ^ 4 =
    (P x * Q z) ^ 2 * Q x

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

Tactic:
ring1

Result:
no goals