harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem sup_vanishingIdeal_le (t t' : Set (PrimeSpectrum R)) :
    vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Proof state:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Tactic:
apply Submodule.add_mem <;> solve_by_elim

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Tactic:
rw [mem_vanishingIdeal] at hf hg

Result:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ x ∈ t, f ∈ x.asIdeal
g : R
hg : ∀ x ∈ t', g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal

Tactic:
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩

Result:
case intro.intro.intro.intro.intro
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')

Tactic:
rw [Submodule.mem_sup, mem_vanishingIdeal]

Result:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y ∈ vanishingIdeal t, ∃ z ∈ vanishingIdeal t', y + z = r) → ∀ x ∈ t ∩ t', r ∈ x.asIdeal

Proof state:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')

Tactic:
intro r

Result:
R : Type u
inst✝ : CommSemiring R
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
-- Mathlib/RingTheory/Adjoin/FG.lean
theorem FG.prod {S : Subalgebra R A} {T : Subalgebra R B} (hS : S.FG) (hT : T.FG) :
    (S.prod T).FG

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
⊢ (S.prod T).FG

Tactic:
obtain ⟨s, hs⟩ := fg_def.1 hS

Result:
case intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
⊢ (S.prod T).FG

Proof state:
case intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
⊢ (S.prod T).FG

Tactic:
obtain ⟨t, ht⟩ := fg_def.1 hT

Result:
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ (S.prod T).FG

Proof state:
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ (S.prod T).FG

Tactic:
rw [← hs.2, ← ht.2]

Result:
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ ((Algebra.adjoin R s).prod (Algebra.adjoin R t)).FG

Proof state:
case intro.intro
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S : Subalgebra R A
T : Subalgebra R B
hS : S.FG
hT : T.FG
s : Set A
hs : s.Finite ∧ Algebra.adjoin R s = S
t : Set B
ht : t.Finite ∧ Algebra.adjoin R t = T
⊢ ((Algebra.adjoin R s).prod (Algebra.adjoin R t)).FG

Tactic:
exact fg_def.2 ⟨LinearMap.inl R A B '' (s ∪ {1}) ∪ LinearMap.inr R A B '' (t ∪ {1}),
  Set.Finite.union (Set.Finite.image _ (Set.Finite.union hs.1 (Set.finite_singleton _)))
    (Set.Finite.image _ (Set.Finite.union ht.1 (Set.finite_singleton _))),
  Algebra.adjoin_inl_union_inr_eq_prod R s t⟩

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem intPow_negOfNat_bit1 {b' c' : ℕ} (h1 : Nat.pow a b' = c')
    (hb : nat_lit 2 * b' + nat_lit 1 = b) (hc : c' * (c' * a) = c) :
    Int.pow (Int.negOfNat a) b = Int.negOfNat c

Proof state:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))

Tactic:
simp [mul_assoc, mul_comm, mul_left_comm]

Result:
no goals

Proof state:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ (Int.negOfNat a).pow b = Int.negOfNat c

Tactic:
rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, Int.pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul,
  two_mul, pow_add, ← hc, ← h1]

Result:
a b c b' c' : ℕ
h1 : a.pow b' = c'
hb : 2 * b' + 1 = b
hc : c' * (c' * a) = c
⊢ Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma nnrpow_one (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun x => x) a = a

Tactic:
change cfcₙ (id : ℝ≥0 → ℝ≥0) a = a

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ id a = a

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ id a = a

Tactic:
rw [cfcₙ_id ℝ≥0 a]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 1 = a

Tactic:
simp only [nnrpow_def, NNReal.nnrpow_def, NNReal.coe_one, NNReal.rpow_one]

Result:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ cfcₙ (fun x => x) a = a
-- Mathlib/Data/Finset/Image.lean
theorem mem_image_const : c ∈ s.image (const α b) ↔ s.Nonempty ∧ b = c

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ c ∈ image (const α b) s ↔ s.Nonempty ∧ b = c

Tactic:
rw [mem_image]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ (∃ a ∈ s, const α b a = c) ↔ s.Nonempty ∧ b = c

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ (∃ a ∈ s, const α b a = c) ↔ s.Nonempty ∧ b = c

Tactic:
simp only [exists_prop, const_apply, exists_and_right]

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ (∃ x, x ∈ s) ∧ b = c ↔ s.Nonempty ∧ b = c

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
b c : β
⊢ (∃ x, x ∈ s) ∧ b = c ↔ s.Nonempty ∧ b = c

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem log_zpow (x : ℝ) (n : ℤ) : log (x ^ n) = n * log x

Proof state:
case ofNat
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x

Tactic:
rw [Int.ofNat_eq_coe, zpow_natCast, log_pow, Int.cast_natCast]

Result:
no goals

Proof state:
x : ℝ
n : ℤ
⊢ log (x ^ n) = ↑n * log x

Tactic:
cases n

Result:
case ofNat
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.ofNat a✝) = ↑(Int.ofNat a✝) * log x

case negSucc
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x

Proof state:
case negSucc
x : ℝ
a✝ : ℕ
⊢ log (x ^ Int.negSucc a✝) = ↑(Int.negSucc a✝) * log x

Tactic:
rw [zpow_negSucc, log_inv, log_pow, Int.cast_negSucc, Nat.cast_add_one, neg_mul_eq_neg_mul]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem eq_or_mem_of_mem_cons {a b : α} {s : Stream' α} : (a ∈ b::s) → a = b ∨ a ∈ s :=
    fun ⟨n, h⟩ => by
  rcases n with - | n'
  · left
    exact h
  · right
    rw [get_succ, tail_cons] at h
    exact ⟨n', h⟩

Proof state:
case zero.h
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b

Tactic:
exact h

Result:
no goals

Proof state:
case succ.h
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = s.get n'
⊢ a ∈ s

Tactic:
exact ⟨n', h⟩

Result:
no goals

Proof state:
case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s

Tactic:
right

Result:
case succ.h
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a ∈ s

Proof state:
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n : ℕ
h : (fun b => a = b) ((b :: s).get n)
⊢ a = b ∨ a ∈ s

Tactic:
rcases n with - | n'

Result:
case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s

case succ
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a = b ∨ a ∈ s

Proof state:
case zero
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b ∨ a ∈ s

Tactic:
left

Result:
case zero.h
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
h : a = (b :: s).get 0
⊢ a = b

Proof state:
case succ.h
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = (b :: s).get (n' + 1)
⊢ a ∈ s

Tactic:
rw [get_succ, tail_cons] at h

Result:
case succ.h
α : Type u
a b : α
s : Stream' α
x✝ : a ∈ b :: s
n' : ℕ
h : a = s.get n'
⊢ a ∈ s
-- Mathlib/Computability/Language.lean
lemma mem_kstar_iff_exists_nonempty {x : List α} :
    x ∈ l∗ ↔ ∃ S : List (List α), x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

Proof state:
case mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []) → x ∈ l∗

Tactic:
rintro ⟨S, hx, h⟩

Result:
case mpr.intro.intro
α : Type u_1
l : Language α
x : List α
S : List (List α)
hx : x = S.flatten
h : ∀ y ∈ S, y ∈ l ∧ y ≠ []
⊢ x ∈ l∗

Proof state:
case mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ filter (fun l => !l.isEmpty) S
⊢ y ∈ l ∧ y ≠ []

Tactic:
simp only [mem_filter, Bool.not_eq_eq_eq_not, Bool.not_true, isEmpty_eq_false, ne_eq] at hy

Result:
case mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []

Proof state:
case mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ ∃ S_1, S.flatten = S_1.flatten ∧ ∀ y ∈ S_1, y ∈ l ∧ y ≠ []

Tactic:
refine ⟨S.filter fun l ↦ !List.isEmpty l,
  by simp [List.flatten_filter_not_isEmpty], fun y hy ↦ ?_⟩

Result:
case mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ filter (fun l => !l.isEmpty) S
⊢ y ∈ l ∧ y ≠ []

Proof state:
case mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []

Tactic:
exact ⟨h y hy.1, hy.2⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ → ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

Tactic:
rintro ⟨S, rfl, h⟩

Result:
case mp.intro.intro
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ ∃ S_1, S.flatten = S_1.flatten ∧ ∀ y ∈ S_1, y ∈ l ∧ y ≠ []

Proof state:
α : Type u_1
l : Language α
S : List (List α)
h : ∀ y ∈ S, y ∈ l
⊢ S.flatten = (filter (fun l => !l.isEmpty) S).flatten

Tactic:
simp [List.flatten_filter_not_isEmpty]

Result:
no goals

Proof state:
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ ↔ ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

Tactic:
constructor

Result:
case mp
α : Type u_1
l : Language α
x : List α
⊢ x ∈ l∗ → ∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []

case mpr
α : Type u_1
l : Language α
x : List α
⊢ (∃ S, x = S.flatten ∧ ∀ y ∈ S, y ∈ l ∧ y ≠ []) → x ∈ l∗

Proof state:
case mpr.intro.intro
α : Type u_1
l : Language α
x : List α
S : List (List α)
hx : x = S.flatten
h : ∀ y ∈ S, y ∈ l ∧ y ≠ []
⊢ x ∈ l∗

Tactic:
exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_some {X Y : F} (h : W.Nonsingular ![X, Y, 1]) :
    toAffine W ![X, Y, 1] = .some ((nonsingular_some ..).mp h)

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
X Y : F
h : W.Nonsingular ![X, Y, 1]
⊢ toAffine W ![X, Y, 1] = Affine.Point.some ⋯

Tactic:
simp only [toAffine_of_Z_ne_zero h one_ne_zero, fin3_def_ext, one_pow, div_one]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioi_deriv_of_nonpos' (hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x)
    (g'neg : ∀ x ∈ Ioi a, g' x ≤ 0) (hg : Tendsto g atTop (𝓝 l)) : IntegrableOn g' (Ioi a)

Proof state:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn g' (Ioi a) volume

Tactic:
refine integrableOn_Ioi_deriv_of_nonpos ?_ (fun x hx ↦ hderiv x hx.out.le) g'neg hg

Result:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Proof state:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact (hderiv a left_mem_Ici).continuousAt.continuousWithinAt

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem update_eq_erase : f.update i 0 = f.erase i

Proof state:
case h.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update i 0) j = (erase i f) j

Tactic:
simp [hi.symm]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ f.update i 0 = erase i f

Tactic:
ext j

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (f.update i 0) j = (erase i f) j

Proof state:
case h.inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ (f.update i 0) i = (erase i f) i

Tactic:
simp

Result:
no goals

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (f.update i 0) j = (erase i f) j

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Result:
case h.inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ (f.update i 0) i = (erase i f) i

case h.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update i 0) j = (erase i f) j
-- Mathlib/Algebra/RingQuot.lean
theorem ringQuotToIdealQuotient_apply (r : B → B → Prop) (x : B) :
    ringQuotToIdealQuotient r (mkRingHom r x) = Ideal.Quotient.mk (Ideal.ofRel r) x

Proof state:
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (ringQuotToIdealQuotient r) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
simp_rw [ringQuotToIdealQuotient, lift_def, preLift_def, mkRingHom_def]

Result:
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ ({
          toFun := fun f =>
            { toFun := fun x => Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F =>
            ⟨F.comp
                { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩)
      ({ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x) =
    (Ideal.Quotient.mk (Ideal.ofRel r)) x

Proof state:
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ ({
          toFun := fun f =>
            { toFun := fun x => Quot.lift ⇑↑f ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ },
          invFun := fun F =>
            ⟨F.comp
                { toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨Ideal.Quotient.mk (Ideal.ofRel r), ⋯⟩)
      ({ toFun := fun x => { toQuot := Quot.mk (Rel r) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
          map_add' := ⋯ }
        x) =
    (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_dropLast (xs : List α) (h) :
    xs.dropLast.head h = xs.head (by rintro rfl; simp at h)

Proof state:
case cons.nil
α : Type u_1
x : α
h : [x].dropLast ≠ []
⊢ [x].dropLast.head h = [x].head ⋯

Tactic:
simp at h

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
h : (x :: xs).dropLast ≠ []
⊢ (x :: xs).dropLast.head h = (x :: xs).head ⋯

Tactic:
cases xs with
| nil => simp at h
| cons y ys => rfl

Result:
no goals

Proof state:
case cons.cons
α : Type u_1
x y : α
ys : List α
h : (x :: y :: ys).dropLast ≠ []
⊢ (x :: y :: ys).dropLast.head h = (x :: y :: ys).head ⋯

Tactic:
rfl

Result:
no goals

Proof state:
case nil
α : Type u_1
h : [].dropLast ≠ []
⊢ [].dropLast.head h = [].head ⋯

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
xs : List α
h : xs.dropLast ≠ []
⊢ xs.dropLast.head h = xs.head ⋯

Tactic:
cases xs with
| nil => rfl
| cons x xs =>
  cases xs with
  | nil => simp at h
  | cons y ys => rfl

Result:
no goals

Proof state:
α : Type ?u.327443
xs : List α
h : xs.dropLast ≠ []
⊢ xs ≠ []

Tactic:
rintro rfl

Result:
α : Type ?u.327443
h : [].dropLast ≠ []
⊢ False

Proof state:
α : Type ?u.327443
h : [].dropLast ≠ []
⊢ False

Tactic:
simp at h

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem bind_pure' (s : Computation α) : bind s pure = s

Proof state:
α : Type u
s : Computation α
⊢ s.bind pure = s

Tactic:
apply eq_of_bisim fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = bind s pure ∧ c₂ = s

Result:
case bisim
α : Type u
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s

case r
α : Type u
s : Computation α
⊢ s.bind pure = s ∨ ∃ s_1, s.bind pure = s_1.bind pure ∧ s = s_1

Proof state:
case r
α : Type u
s : Computation α
⊢ s.bind pure = s ∨ ∃ s_1, s.bind pure = s_1.bind pure ∧ s = s_1

Tactic:
exact Or.inr ⟨s, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u
s✝ c₁ c₂ : Computation α
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s
s : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s) (s.bind pure).destruct s.destruct

Tactic:
apply recOn s <;> intro s <;> simp

Result:
no goals

Proof state:
α : Type u
s c₁ c₂✝ : Computation α
h : c₁ = c₂✝ ∨ ∃ s, c₁ = s.bind pure ∧ c₂✝ = s
c₂ : Computation α
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s) c₂.destruct c₂.destruct

Tactic:
rcases destruct c₂ with b | cb <;> simp

Result:
no goals

Proof state:
case bisim
α : Type u
s c₁ c₂ : Computation α
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s) c₁.destruct c₂.destruct

Tactic:
match c₁, c₂, h with
| _, c₂, Or.inl (Eq.refl _) => rcases destruct c₂ with b | cb <;> simp
| _, _, Or.inr ⟨s, rfl, rfl⟩ =>
  apply recOn s <;> intro s <;> simp

Result:
no goals

Proof state:
case bisim
α : Type u
s : Computation α
⊢ IsBisimulation fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s

Tactic:
intro c₁ c₂ h

Result:
case bisim
α : Type u
s c₁ c₂ : Computation α
h : c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s
⊢ BisimO (fun c₁ c₂ => c₁ = c₂ ∨ ∃ s, c₁ = s.bind pure ∧ c₂ = s) c₁.destruct c₂.destruct
-- Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean
theorem ker_aeval_ring_hom'_unit_polynomial (f : End K V) (c : K[X]ˣ) :
    LinearMap.ker (aeval f (c : K[X])) = ⊥

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker ((aeval f) (C ((↑c).coeff 0))) = ⊥

Tactic:
simp only [aeval_def, eval₂_C]

Result:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker ((algebraMap K (End K V)) ((↑c).coeff 0)) = ⊥

Proof state:
case ha
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ (↑c).coeff 0 ≠ 0

Tactic:
apply coeff_coe_units_zero_ne_zero c

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker ((aeval f) ↑c) = ⊥

Tactic:
rw [Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]

Result:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker ((aeval f) (C ((↑c).coeff 0))) = ⊥

Proof state:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ LinearMap.ker ((algebraMap K (End K V)) ((↑c).coeff 0)) = ⊥

Tactic:
apply ker_algebraMap_end

Result:
case ha
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
c : K[X]ˣ
⊢ (↑c).coeff 0 ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_ofList_of_contains_eq_false [LawfulBEq α]
    {l : List (α × β)} {k : α} {fallback : β}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    getD (ofList l) k fallback = fallback

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
fallback : β
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ getD (ofList l) k fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem C_ne_zero {r : R} (h : r ≠ 0) : (C r : HahnSeries Γ R) ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : C r = 0
⊢ r = 0

Tactic:
rw [← C_zero] at h

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : C r = C 0
⊢ r = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : C r = C 0
⊢ r = 0

Tactic:
exact C_injective h

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : r ≠ 0
⊢ C r ≠ 0

Tactic:
contrapose! h

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r : R
h : C r = 0
⊢ r = 0