harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem mk_injective (A B : T) :
    Function.Injective (Arrow.mk : (A ⟶ B) → Arrow T) := fun f g h => by
  cases h
  rfl

Proof state:
T : Type u
inst✝ : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g

Tactic:
cases h

Result:
case refl
T : Type u
inst✝ : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f

Proof state:
case refl
T : Type u
inst✝ : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem smul_eq_mul : ∀ (n : ℕ) (a : Ordinal), n • a = a * n
  | 0, a => by rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | n + 1, a => by rw [succ_nsmul, Nat.cast_add, mul_add, Nat.cast_one, mul_one, smul_eq_mul n]

Proof state:
n : ℕ
a : Ordinal.{u_4}
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
rw [succ_nsmul, Nat.cast_add, mul_add, Nat.cast_one, mul_one, smul_eq_mul n]

Result:
no goals

Proof state:
a : Ordinal.{u_4}
⊢ 0 • a = a * ↑0

Tactic:
rw [zero_nsmul, Nat.cast_zero, mul_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem norm_setIntegral_le_of_norm_le_const_ae'' {C : ℝ} (hs : μ s < ∞) (hsm : MeasurableSet s)
    (hC : ∀ᵐ x ∂μ, x ∈ s → ‖f x‖ ≤ C) : ‖∫ x in s, f x ∂μ‖ ≤ C * (μ s).toReal :=
  norm_setIntegral_le_of_norm_le_const_ae hs <| by
    rwa [ae_restrict_eq hsm, eventually_inf_principal]

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ⊤
hsm : MeasurableSet s
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
⊢ ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C

Tactic:
rwa [ae_restrict_eq hsm, eventually_inf_principal]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_surjective : Function.Surjective cos

Proof state:
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ cexp (log w / I * I) ^ 2 - 2 * x * cexp (log w / I * I) + 1 = 0

Tactic:
rw [div_mul_cancel₀ _ I_ne_zero, exp_log w₀]

Result:
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0

Proof state:
case intro
x w : ℂ
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ≠ 0

Tactic:
rintro rfl

Result:
case intro
x : ℂ
hw : 1 * (0 * 0) + -2 * x * 0 + 1 = 0
⊢ False

Proof state:
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ ∃ a, cos a = x

Tactic:
refine ⟨log w / I, cos_eq_iff_quadratic.2 ?_⟩

Result:
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ cexp (log w / I * I) ^ 2 - 2 * x * cexp (log w / I * I) + 1 = 0

Proof state:
case h.e'_2
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 1 * (w * w) + -2 * x * w + 1

Tactic:
ring

Result:
no goals

Proof state:
x : ℂ
⊢ ∃ a, cos a = x

Tactic:
obtain ⟨w, w₀, hw⟩ : ∃ w ≠ 0, 1 * (w * w) + -2 * x * w + 1 = 0 := by
  rcases exists_quadratic_eq_zero one_ne_zero
      ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
    ⟨w, hw⟩
  refine ⟨w, ?_, hw⟩
  rintro rfl
  simp only [zero_add, one_ne_zero, mul_zero] at hw

Result:
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ ∃ a, cos a = x

Proof state:
⊢ Function.Surjective cos

Tactic:
intro x

Result:
x : ℂ
⊢ ∃ a, cos a = x

Proof state:
x : ℂ
⊢ ∃ w, w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0

Tactic:
rcases exists_quadratic_eq_zero one_ne_zero
    ⟨_, (cpow_nat_inv_pow _ two_ne_zero).symm.trans <| pow_two _⟩ with
  ⟨w, hw⟩

Result:
case intro
x w : ℂ
hw : 1 * (w * w) + ?m.71611 * w + ?m.71612 = 0
⊢ ∃ w, w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0

Proof state:
case intro.intro
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 0

Tactic:
convert hw using 1

Result:
case h.e'_2
x w : ℂ
w₀ : w ≠ 0
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ^ 2 - 2 * x * w + 1 = 1 * (w * w) + -2 * x * w + 1

Proof state:
case intro
x w : ℂ
hw : 1 * (w * w) + ?m.71611 * w + ?m.71612 = 0
⊢ ∃ w, w ≠ 0 ∧ 1 * (w * w) + -2 * x * w + 1 = 0

Tactic:
refine ⟨w, ?_, hw⟩

Result:
case intro
x w : ℂ
hw : 1 * (w * w) + -2 * x * w + 1 = 0
⊢ w ≠ 0

Proof state:
case intro
x : ℂ
hw : 1 * (0 * 0) + -2 * x * 0 + 1 = 0
⊢ False

Tactic:
simp only [zero_add, one_ne_zero, mul_zero] at hw

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem wordProd_surjective : Surjective cs.wordProd

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Surjective cs.wordProd

Tactic:
intro w

Result:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ a, cs.wordProd a = w

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ a, cs.wordProd a = w

Tactic:
apply cs.simple_induction_left w

Result:
case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ a, cs.wordProd a = 1

case mul_simple_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∀ (w : W) (i : B), (∃ a, cs.wordProd a = w) → ∃ a, cs.wordProd a = cs.simple i * w

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

Tactic:
rw [wordProd_cons]

Result:
no goals

Proof state:
case one
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∃ a, cs.wordProd a = 1

Tactic:
use []

Result:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.wordProd [] = 1

Proof state:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.wordProd [] = 1

Tactic:
rw [wordProd_nil]

Result:
no goals

Proof state:
case mul_simple_left.intro
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ ∃ a, cs.wordProd a = cs.simple i * cs.wordProd ω

Tactic:
use i :: ω

Result:
case h
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Proof state:
case mul_simple_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∀ (w : W) (i : B), (∃ a, cs.wordProd a = w) → ∃ a, cs.wordProd a = cs.simple i * w

Tactic:
rintro _ i ⟨ω, rfl⟩

Result:
case mul_simple_left.intro
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
ω : List B
⊢ ∃ a, cs.wordProd a = cs.simple i * cs.wordProd ω
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem length_eq_countP_add_countP (l) : length l = countP p l + countP (fun a => ¬p a) l

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ [].length = countP p [] + countP (fun a => decide ¬p a = true) []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (fun a => decide ¬p a = true) x = true

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ countP p h✝ + countP (fun a => decide ¬p a = true) h✝ + 1 =
    countP p h✝ + (countP (fun a => decide ¬p a = true) h✝ + 1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (x :: h✝).length = countP p (x :: h✝) + countP (fun a => decide ¬p a = true) (x :: h✝)

Tactic:
rw [countP_cons_of_pos (fun a => ¬p a) _ _, countP_cons_of_neg _ _ h, length, ih]

Result:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ countP p h✝ + countP (fun a => decide ¬p a = true) h✝ + 1 =
    countP p h✝ + (countP (fun a => decide ¬p a = true) h✝ + 1)

α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : ¬p x = true
⊢ (fun a => decide ¬p a = true) x = true

Proof state:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ (x :: h✝).length = countP p (x :: h✝) + countP (fun a => decide ¬p a = true) (x :: h✝)

Tactic:
rw [countP_cons_of_pos _ _ h, countP_cons_of_neg _ _ _, length, ih]

Result:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ countP p h✝ + countP (fun a => decide ¬p a = true) h✝ + 1 = countP p h✝ + 1 + countP (fun a => decide ¬p a = true) h✝

α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ ¬(decide ¬p x = true) = true

Proof state:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ countP p h✝ + countP (fun a => decide ¬p a = true) h✝ + 1 = countP p h✝ + 1 + countP (fun a => decide ¬p a = true) h✝

Tactic:
rw [Nat.add_assoc, Nat.add_comm _ 1, Nat.add_assoc]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
h✝ : List α
ih : h✝.length = countP p h✝ + countP (fun a => decide ¬p a = true) h✝
h : p x = true
⊢ ¬(decide ¬p x = true) = true

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem Max.right_comm (a b c : α) : max (max a b) c = max (max a c) b

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b

Tactic:
rw [max_assoc, max_comm b, max_assoc]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem mem_zeroRootSubalgebra (x : L) :
    x ∈ zeroRootSubalgebra R L H ↔ ∀ y : H, ∃ k : ℕ, (toEnd R H L y ^ k) x = 0

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
⊢ x ∈ rootSpace H 0 ↔ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
simp only [mem_genWeightSpace, Pi.zero_apply, zero_smul, sub_zero]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
⊢ x ∈ zeroRootSubalgebra R L H ↔ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0

Tactic:
change x ∈ rootSpace H 0 ↔ _

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
x : L
⊢ x ∈ rootSpace H 0 ↔ ∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) x = 0
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem abs_sub_le_of_uIcc_subset_uIcc (h : [[c, d]] ⊆ [[a, b]]) : |d - c| ≤ |b - a|

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ⊓ b ≤ c ⊓ d ∧ c ⊔ d ≤ a ⊔ b
⊢ c ⊔ d - c ⊓ d ≤ a ⊔ b - a ⊓ b

Tactic:
exact sub_le_sub h.2 h.1

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ c ⊔ d - c ⊓ d ≤ a ⊔ b - a ⊓ b

Tactic:
rw [uIcc_subset_uIcc_iff_le] at h

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : a ⊓ b ≤ c ⊓ d ∧ c ⊔ d ≤ a ⊔ b
⊢ c ⊔ d - c ⊓ d ≤ a ⊔ b - a ⊓ b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ |d - c| ≤ |b - a|

Tactic:
rw [← max_sub_min_eq_abs, ← max_sub_min_eq_abs]

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
h : [[c, d]] ⊆ [[a, b]]
⊢ c ⊔ d - c ⊓ d ≤ a ⊔ b - a ⊓ b
-- Mathlib/GroupTheory/Nilpotent.lean
theorem lowerCentralSeries_eq_bot_iff_nilpotencyClass_le {n : ℕ} :
    lowerCentralSeries G n = ⊥ ↔ Group.nilpotencyClass G ≤ n

Proof state:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_le h

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ lowerCentralSeries G (nilpotencyClass G)

Tactic:
exact lowerCentralSeries_antitone h

Result:
no goals

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → lowerCentralSeries G n = ⊥

Tactic:
intro h

Result:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n = ⊥

Proof state:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ nilpotencyClass G ≤ n

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Result:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ Nat.find ⋯ ≤ n

Proof state:
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ ↔ nilpotencyClass G ≤ n

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ → nilpotencyClass G ≤ n

case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → lowerCentralSeries G n = ⊥

Proof state:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ → nilpotencyClass G ≤ n

Tactic:
intro h

Result:
case mp
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ nilpotencyClass G ≤ n

Proof state:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n = ⊥

Tactic:
rw [eq_bot_iff, ← lowerCentralSeries_nilpotencyClass]

Result:
case mpr
G : Type u_1
inst✝ : Group G
hG : IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ lowerCentralSeries G (nilpotencyClass G)
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_neg' (a b : α) : toIcoMod hp (-a) b = p - toIocMod hp a (-b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp (-a) b = p - toIocMod hp a (-b)

Tactic:
simpa only [neg_neg] using toIcoMod_neg hp (-a) (-b)

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem mem_sInf {S : Set (StarSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : Set (StarSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem hermite_eq_iterate (n : ℕ) : hermite n = (fun p => X * p - derivative p)^[n] 1

Proof state:
case succ
n : ℕ
ih : hermite n = (fun p => X * p - derivative p)^[n] 1
⊢ hermite (n + 1) = (fun p => X * p - derivative p)^[n + 1] 1

Tactic:
rw [Function.iterate_succ_apply', ← ih, hermite_succ]

Result:
no goals

Proof state:
case zero

⊢ hermite 0 = (fun p => X * p - derivative p)^[0] 1

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ hermite n = (fun p => X * p - derivative p)^[n] 1

Tactic:
induction n with
| zero => rfl
| succ n ih => rw [Function.iterate_succ_apply', ← ih, hermite_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_udiv_of_msb {x : BitVec w} (h : x.msb = false) (y : BitVec w) :
    (x / y).toInt = x.toNat / y.toNat

Proof state:
w : Nat
x : BitVec w
h : x.msb = false
y : BitVec w
⊢ (x / y).toInt = ↑x.toNat / ↑y.toNat

Tactic:
simp [toInt_eq_msb_cond, msb_udiv_eq_false_of h]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem mul_mem_mul {I J : FractionalIdeal S P} {i j : P} (hi : i ∈ I) (hj : j ∈ J) :
    i * j ∈ I * J

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
i j : P
hi : i ∈ I
hj : j ∈ J
⊢ i * j ∈ ⟨↑I * ↑J, ⋯⟩

Tactic:
exact Submodule.mul_mem_mul hi hj

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
i j : P
hi : i ∈ I
hj : j ∈ J
⊢ i * j ∈ I * J

Tactic:
simp only [mul_def]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : FractionalIdeal S P
i j : P
hi : i ∈ I
hj : j ∈ J
⊢ i * j ∈ ⟨↑I * ↑J, ⋯⟩
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
lemma δAux_mul (x y) :
    δAux R Q (x * y) = x • (δAux R Q y) + y • (δAux R Q x)

Proof state:
case h1.h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
m : Q.vars →₀ ℕ
s : S
⊢ ((algebraMap S T) r * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * (n + m).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) r =
    ((algebraMap S T) r * ((n.prod fun x1 x2 => Q.val x1 ^ x2) * m.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) s +
      ((algebraMap S T) s * ((n.prod fun x1 x2 => Q.val x1 ^ x2) * m.prod fun x1 x2 => Q.val x1 ^ x2)) ⊗ₜ[S] (D R S) r

Tactic:
simp only [pow_zero, implies_true, pow_add, Finsupp.prod_add_index']

Result:
no goals

Proof state:
case h1.h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
n : Q.vars →₀ ℕ
r : S
y₁ y₂ : MvPolynomial Q.vars S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r) +
      ((monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)) =
    (monomial n) r • (δAux R Q) y₁ + (monomial n) r • (δAux R Q) y₂ +
      (y₁ • (δAux R Q) ((monomial n) r) + y₂ • (δAux R Q) ((monomial n) r))

Tactic:
abel

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
x y : Q.Ring
⊢ (δAux R Q) (x * y) = x • (δAux R Q) y + y • (δAux R Q) x

Tactic:
induction' x using MvPolynomial.induction_on' with n r x₁ x₂ hx₁ hx₂

Result:
case h1
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
y : Q.Ring
n : Q.vars →₀ ℕ
r : S
⊢ (δAux R Q) ((monomial n) r * y) = (monomial n) r • (δAux R Q) y + y • (δAux R Q) ((monomial n) r)

case h2
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
y : Q.Ring
x₁ x₂ : MvPolynomial Q.vars S
hx₁ : (δAux R Q) (x₁ * y) = x₁ • (δAux R Q) y + y • (δAux R Q) x₁
hx₂ : (δAux R Q) (x₂ * y) = x₂ • (δAux R Q) y + y • (δAux R Q) x₂
⊢ (δAux R Q) ((x₁ + x₂) * y) = (x₁ + x₂) • (δAux R Q) y + y • (δAux R Q) (x₁ + x₂)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem mul_congr (w : Nat) (lhs rhs lhs' rhs' : BitVec w) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
    lhs' * rhs' = lhs * rhs

Proof state:
w : Nat
lhs rhs lhs' rhs' : BitVec w
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' * rhs' = lhs * rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem eq_pow_of_factorization_eq_single {n p k : ℕ} (hn : n ≠ 0)
    (h : n.factorization = Finsupp.single p k) : n = p ^ k

Proof state:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ p ^ 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ n = p ^ k

Tactic:
rw [← Nat.factorization_prod_pow_eq_self hn, h, Finsupp.prod_single_index]

Result:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ p ^ 0 = 1
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem Filter.EventuallyEq.lineDeriv_eq (h : f₁ =ᶠ[𝓝 x] f) :
    lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₁ : E → F
x v : E
h : f₁ =ᶠ[𝓝 x] f
⊢ lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v

Tactic:
rw [← lineDerivWithin_univ, ← lineDerivWithin_univ, h.lineDerivWithin_eq_nhds]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem interpolate_singleton : interpolate {i} v r = C (r i)

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
i : ι
v r : ι → F
⊢ (interpolate {i} v) r = C (r i)

Tactic:
rw [interpolate_apply, sum_singleton, basis_singleton, mul_one]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem mem_interedges_iff {x : α × β} : x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
⊢ x ∈ interedges r s t ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2

Tactic:
rw [interedges, mem_filter, Finset.mem_product, and_assoc]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma toReal_eq_toReal {x y : EReal} (hx_top : x ≠ ⊤) (hx_bot : x ≠ ⊥)
    (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) :
    x.toReal = y.toReal ↔ x = y

Proof state:
x y : EReal
hx_top : x ≠ ⊤
hx_bot : x ≠ ⊥
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
⊢ x.toReal = y.toReal ↔ x = y

Tactic:
lift x to ℝ using ⟨hx_top, hx_bot⟩

Result:
case intro
y : EReal
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
x : ℝ
hx_top : ↑x ≠ ⊤
hx_bot : ↑x ≠ ⊥
⊢ (↑x).toReal = y.toReal ↔ ↑x = y

Proof state:
case intro.intro
x : ℝ
hx_top : ↑x ≠ ⊤
hx_bot : ↑x ≠ ⊥
y : ℝ
hy_top : ↑y ≠ ⊤
hy_bot : ↑y ≠ ⊥
⊢ (↑x).toReal = (↑y).toReal ↔ ↑x = ↑y

Tactic:
simp

Result:
no goals

Proof state:
case intro
y : EReal
hy_top : y ≠ ⊤
hy_bot : y ≠ ⊥
x : ℝ
hx_top : ↑x ≠ ⊤
hx_bot : ↑x ≠ ⊥
⊢ (↑x).toReal = y.toReal ↔ ↑x = y

Tactic:
lift y to ℝ using ⟨hy_top, hy_bot⟩

Result:
case intro.intro
x : ℝ
hx_top : ↑x ≠ ⊤
hx_bot : ↑x ≠ ⊥
y : ℝ
hy_top : ↑y ≠ ⊤
hy_bot : ↑y ≠ ⊥
⊢ (↑x).toReal = (↑y).toReal ↔ ↑x = ↑y