harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.eq_of_smul_apply_eq_smul_apply {M : Type*} [AddCommMonoid M] [Module R M]
    {v : ι → M} (li : LinearIndependent R v) (c d : R) (i j : ι) (hc : c ≠ 0)
    (h : c • v i = d • v j) : i = j

Proof state:
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ i = j

Tactic:
have h_single_eq : Finsupp.single i c = Finsupp.single j d :=
  li <| by simpa [Finsupp.linearCombination_apply] using h

Result:
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
⊢ i = j

Proof state:
case inr.intro
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc✝ : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
hc : c = 0
right✝ : d = 0
⊢ i = j

Tactic:
contradiction

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
⊢ (Finsupp.linearCombination R v) (Finsupp.single i c) = (Finsupp.linearCombination R v) (Finsupp.single j d)

Tactic:
simpa [Finsupp.linearCombination_apply] using h

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
⊢ i = j

Tactic:
rcases (Finsupp.single_eq_single_iff ..).mp h_single_eq with (⟨H, _⟩ | ⟨hc, _⟩)

Result:
case inl.intro
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
H : i = j
right✝ : c = d
⊢ i = j

case inr.intro
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc✝ : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
hc : c = 0
right✝ : d = 0
⊢ i = j

Proof state:
case inl.intro
ι : Type u'
R : Type u_2
inst✝² : Semiring R
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
li : LinearIndependent R v
c d : R
i j : ι
hc : c ≠ 0
h : c • v i = d • v j
h_single_eq : Finsupp.single i c = Finsupp.single j d
H : i = j
right✝ : c = d
⊢ i = j

Tactic:
exact H

Result:
no goals
-- Mathlib/Algebra/Ring/Invertible.lean
theorem invOf_sub_invOf [Ring α] (a b : α) [Invertible a] [Invertible b] :
    ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

Proof state:
α : Type u
inst✝² : Ring α
a b : α
inst✝¹ : Invertible a
inst✝ : Invertible b
⊢ ⅟a - ⅟b = ⅟a * (b - a) * ⅟b

Tactic:
rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
    (modify f n l)[m] =
      if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega)

Proof state:
α : Type ?u.23015
f : α → α
n : Nat
l : List α
m : Nat
h : m < l.length
⊢ m < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h : m < (modify f n l).length
⊢ (modify f n l)[m] = if n = m then f l[m] else l[m]

Tactic:
rw [getElem_eq_iff, getElem?_modify]

Result:
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h : m < (modify f n l).length
⊢ (fun a => if n = m then f a else a) <$> l[m]? = some (if n = m then f l[m] else l[m])

Proof state:
α : Type ?u.23015
f : α → α
n : Nat
l : List α
m : Nat
h : m < (modify f n l).length
⊢ m < l.length

Tactic:
simp at h

Result:
α : Type ?u.23015
f : α → α
n : Nat
l : List α
m : Nat
h : m < l.length
⊢ m < l.length

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h✝ : m < (modify f n l).length
h : m < l.length
⊢ (fun a => if n = m then f a else a) <$> l[m]? = some (if n = m then f l[m] else l[m])

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h : m < (modify f n l).length
⊢ (fun a => if n = m then f a else a) <$> l[m]? = some (if n = m then f l[m] else l[m])

Tactic:
simp at h

Result:
α : Type u_1
f : α → α
n : Nat
l : List α
m : Nat
h✝ : m < (modify f n l).length
h : m < l.length
⊢ (fun a => if n = m then f a else a) <$> l[m]? = some (if n = m then f l[m] else l[m])
-- Mathlib/Data/Set/Countable.lean
lemma enumerateCountable_mem {s : Set α} (h : s.Countable) {default : α} (h_mem : default ∈ s)
    (n : ℕ) :
    enumerateCountable h default n ∈ s

Proof state:
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ enumerateCountable h default n ∈ s

Tactic:
convert mem_range_self n

Result:
case h.e'_4
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ s = range (enumerateCountable h default)

Proof state:
case h.e'_4
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ s = range (enumerateCountable h default)

Tactic:
exact (range_enumerateCountable_of_mem h h_mem).symm

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem kahler_rotation_left (x y : V) (θ : Real.Angle) :
    o.kahler (o.rotation θ x) y = conj (θ.toCircle : ℂ) * o.kahler x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ (o.kahler ((o.rotation θ) x)) y = (starRingEnd ℂ) ↑θ.toCircle * (o.kahler x) y

Tactic:
simp only [o.rotation_apply, map_add, map_mul, LinearMap.map_smulₛₗ, RingHom.id_apply,
  LinearMap.add_apply, LinearMap.smul_apply, real_smul, kahler_rightAngleRotation_left,
  Real.Angle.coe_toCircle, Complex.conj_ofReal, conj_I]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑θ.cos * (o.kahler x) y + ↑θ.sin * (-I * (o.kahler x) y) = (↑θ.cos + ↑θ.sin * -I) * (o.kahler x) y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
θ : Real.Angle
⊢ ↑θ.cos * (o.kahler x) y + ↑θ.sin * (-I * (o.kahler x) y) = (↑θ.cos + ↑θ.sin * -I) * (o.kahler x) y

Tactic:
ring

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.unop {S : ShortComplex Cᵒᵖ} (h : S.Exact) : S.unop.Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.Exact
⊢ S.unop.Exact

Tactic:
obtain ⟨h, z⟩ := h

Result:
case mk.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.HomologyData
z : IsZero h.left.H
⊢ S.unop.Exact

Proof state:
case mk.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.HomologyData
z : IsZero h.left.H
⊢ S.unop.Exact

Tactic:
exact ⟨⟨h.unop, (IsZero.of_iso z h.iso.symm).unop⟩⟩

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem balanced_ball_zero (r : ℝ) : Balanced 𝕜 (ball p 0 r)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
⊢ Balanced 𝕜 (p.ball 0 r)

Tactic:
rintro a ha x ⟨y, hy, hx⟩

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x => a • x) y = x
⊢ x ∈ p.ball 0 r

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x => a • x) y = x
⊢ x ∈ p.ball 0 r

Tactic:
rw [mem_ball_zero, ← hx, map_smul_eq_mul]

Result:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x => a • x) y = x
⊢ ‖a‖ * p y < r

Proof state:
case intro.intro
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x => a • x) y = x
⊢ ‖a‖ * p y < r

Tactic:
calc
  _ ≤ p y := mul_le_of_le_one_left (apply_nonneg p _) ha
  _ < r := by rwa [mem_ball_zero] at hy

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
r : ℝ
a : 𝕜
ha : ‖a‖ ≤ 1
x y : E
hy : y ∈ p.ball 0 r
hx : (fun x => a • x) y = x
⊢ p y < r

Tactic:
rwa [mem_ball_zero] at hy

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setIntegral_rnDeriv_smul (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) :
    ∫ x in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ x in s, f x ∂μ

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

Tactic:
simp_rw [← integral_indicator hs, Set.indicator_smul, integral_rnDeriv_smul hμν]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem div_rpow_of_nonneg (x y : ℝ≥0∞) {z : ℝ} (hz : 0 ≤ z) : (x / y) ^ z = x ^ z / y ^ z

Proof state:
x y : ℝ≥0∞
z : ℝ
hz : 0 ≤ z
⊢ (x / y) ^ z = x ^ z / y ^ z

Tactic:
rw [div_eq_mul_inv, mul_rpow_of_nonneg _ _ hz, inv_rpow, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_le (n m l : ℕ) : ((Ico n m).filter fun x => l ≤ x) = Ico (max n l) m

Proof state:
n m l : ℕ
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (n ⊔ l) m

Tactic:
rcases le_total n l with hnl | hln

Result:
case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (n ⊔ l) m

case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (n ⊔ l) m

Proof state:
case inl
n m l : ℕ
hnl : n ≤ l
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (n ⊔ l) m

Tactic:
rw [max_eq_right hnl, filter_le_of_le hnl]

Result:
no goals

Proof state:
case inr
n m l : ℕ
hln : l ≤ n
⊢ filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (n ⊔ l) m

Tactic:
rw [max_eq_left hln, filter_le_of_le_bot hln]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
/-- A group is made up of a disjoint union of cosets of a subgroup. -/
@[to_additive "An additive group is made up of a disjoint union of cosets of an additive
subgroup."]
lemma univ_eq_iUnion_smul (H : Subgroup α) :
    (Set.univ (α := α)) = ⋃ x : α ⧸ H, x.out • (H : Set _)

Proof state:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ univ = ⋃ x, Quotient.out x • ↑H

Tactic:
simp_rw [univ_eq_iUnion_orbit H.op, orbit_eq_out_smul]

Result:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ ⋃ x, Quotient.out x • ↑H = ⋃ x, Quotient.out x • ↑H

Proof state:
α : Type u_1
inst✝ : Group α
H : Subgroup α
⊢ ⋃ x, Quotient.out x • ↑H = ⋃ x, Quotient.out x • ↑H

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem two_le_iff : (2 : Cardinal) ≤ #α ↔ ∃ x y : α, x ≠ y

Proof state:
α : Type u
⊢ 2 ≤ #α ↔ ∃ x y, x ≠ y

Tactic:
rw [← Nat.cast_two, nat_succ, succ_le_iff, Nat.cast_one, one_lt_iff_nontrivial, nontrivial_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.not_beq_not (a b : BitVec w) : (~~~a == ~~~b) = (a == b)

Proof state:
w : Nat
a b : BitVec w
⊢ (~~~a == ~~~b) = (a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (~~~a == ~~~b) = true ↔ (a == b) = true

Proof state:
w : Nat
a b : BitVec w
⊢ (~~~a == ~~~b) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Order/WellFounded.lean
theorem StrictMono.id_le [WellFoundedLT β] {f : β → β} (hf : StrictMono f) : id ≤ f

Proof state:
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ ∀ (i : β), id i ≤ f i

Tactic:
by_contra! H

Result:
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ i, f i < id i
⊢ False

Proof state:
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ i, f i < id i
⊢ False

Tactic:
obtain ⟨m, hm, hm'⟩ := wellFounded_lt.has_min _ H

Result:
case intro.intro
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ i, f i < id i
m : β
hm : m ∈ fun x => Preorder.toLT.1 (f x) (id x)
hm' : ∀ x ∈ fun x => Preorder.toLT.1 (f x) (id x), ¬x < m
⊢ False

Proof state:
case intro.intro
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
H : ∃ i, f i < id i
m : β
hm : m ∈ fun x => Preorder.toLT.1 (f x) (id x)
hm' : ∀ x ∈ fun x => Preorder.toLT.1 (f x) (id x), ¬x < m
⊢ False

Tactic:
exact hm' _ (hf hm) hm

Result:
no goals

Proof state:
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ id ≤ f

Tactic:
rw [Pi.le_def]

Result:
β : Type u_2
inst✝¹ : LinearOrder β
inst✝ : WellFoundedLT β
f : β → β
hf : StrictMono f
⊢ ∀ (i : β), id i ≤ f i
-- Mathlib/Algebra/Field/Basic.lean
theorem div_add_same (h : b ≠ 0) : (a + b) / b = a / b + 1

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (a + b) / b = a / b + 1

Tactic:
rw [← div_self h, add_div]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem intervalIntegral_preimage (t : ℝ) (f : AddCircle T → E) :
    ∫ a in t..t + T, f a = ∫ b : AddCircle T, f b

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ t ≤ t + T

Tactic:
linarith [hT.out]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ ∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b

Tactic:
rw [integral_of_le, AddCircle.integral_preimage T t f]

Result:
T : ℝ
hT : Fact (0 < T)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
f : AddCircle T → E
⊢ t ≤ t + T
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem linearIndependent_left (H : A.LinearDisjoint L)
    {ι : Type*} {a : ι → A} (ha : LinearIndependent F a) : LinearIndependent L (A.val ∘ a) :=
  (Subalgebra.LinearDisjoint.linearIndependent_left_of_flat H ha).map_of_injective_injective
    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) (AddMonoidHom.id E)
    (by simp) (by simp) (fun _ _ ↦ by simp_rw [Algebra.smul_def]; rfl)

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E) ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹ • x✝) =
    x✝¹ • (AddMonoidHom.id E) x✝

Tactic:
simp_rw [Algebra.smul_def]

Result:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E)
      ((algebraMap (↥(IsScalarTower.toAlgHom F L E).range) E)
          ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹) *
        x✝) =
    (algebraMap L E) x✝¹ * (AddMonoidHom.id E) x✝

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (m : E), (AddMonoidHom.id E) m = 0 → m = 0

Tactic:
simp

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
x✝¹ : L
x✝ : E
⊢ (AddMonoidHom.id E)
      ((algebraMap (↥(IsScalarTower.toAlgHom F L E).range) E)
          ((AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) x✝¹) *
        x✝) =
    (algebraMap L E) x✝¹ * (AddMonoidHom.id E) x✝

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝⁶ : Field F
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
A : IntermediateField F E
L : Type w
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Algebra L E
inst✝ : IsScalarTower F L E
H : A.LinearDisjoint L
ι : Type u_1
a : ι → ↥A
ha : LinearIndependent F a
⊢ ∀ (r : L), (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)) r = 0 → r = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem toIdeal_iInf {κ : Sort*} (s : κ → HomogeneousIdeal 𝒜) :
    (⨅ i, s i).toIdeal = ⨅ i, (s i).toIdeal

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ (⨅ i, s i).toIdeal = ⨅ i, (s i).toIdeal

Tactic:
rw [iInf, toIdeal_sInf, iInf_range]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_eq_quotient_center_plus_one [hH : IsNilpotent G] [Nontrivial G] :
    Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ center G) + 1

Proof state:
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass (G ⧸ center G) + 1

Tactic:
rw [nilpotencyClass_quotient_center]

Result:
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ 0 = 0 - 1 + 1

Tactic:
exfalso

Result:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ False

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = n✝ + 1
⊢ n✝ + 1 = n✝ + 1 - 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ False

Tactic:
rw [nilpotencyClass_zero_iff_subsingleton] at h

Result:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False

Proof state:
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1

Tactic:
rcases h : Group.nilpotencyClass G with ⟨⟩

Result:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ 0 = 0 - 1 + 1

case succ
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = n✝ + 1
⊢ n✝ + 1 = n✝ + 1 - 1 + 1

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False

Tactic:
apply false_of_nontrivial_of_subsingleton G

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma Ψ_two : W.Ψ 2 = W.ψ₂

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ 2 = W.ψ₂

Tactic:
rw [← Nat.cast_two, Ψ_ofNat, preΨ'_two, C_1, one_mul, if_pos even_two]

Result:
no goals
-- Mathlib/Order/CompleteLattice/Finset.lean
theorem iSup_union {f : α → β} {s t : Finset α} :
    ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
f : α → β
s t : Finset α
⊢ ⨆ x ∈ s ∪ t, f x = (⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x

Tactic:
simp [iSup_or, iSup_sup_eq]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
lemma List.iInf_mem_map_of_exists_le_sInf_empty {l : List ι} (f : ι → α)
    (h : ∃ x ∈ l, f x ≤ sInf ∅) :
    ⨅ x ∈ l, f x ∈ l.map f

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ⨅ x ∈ l, f x ∈ map f l

Tactic:
classical
simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ⨅ x ∈ l, f x ∈ map f l

Tactic:
simpa using l.toFinset.ciInf_mem_image f (by simpa using h)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ x ∈ l.toFinset, f x ≤ sInf ∅

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_mul_right_add_left (m n k : ℕ) : gcd (k * n + m) n = gcd m n

Proof state:
m n k : ℕ
⊢ (k * n + m).gcd n = m.gcd n

Tactic:
rw [gcd_comm, gcd_mul_right_add_right, gcd_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@[simp] lemma ae_smul_measure_eq (hc : c ≠ 0) (μ : Measure α) : ae (c • μ) = ae μ

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
s✝ : Set α
⊢ s✝ ∈ ae (c • μ) ↔ s✝ ∈ ae μ

Tactic:
exact ae_smul_measure_iff hc

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
⊢ ae (c • μ) = ae μ

Tactic:
ext

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst✝³ : Zero R
inst✝² : SMulWithZero R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : NoZeroSMulDivisors R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
s✝ : Set α
⊢ s✝ ∈ ae (c • μ) ↔ s✝ ∈ ae μ
-- Mathlib/Data/Sym/Sym2.lean
theorem mk_eq_mk_iff {p q : α × α} : Sym2.mk p = Sym2.mk q ↔ p = q ∨ p = q.swap

Proof state:
α : Type u_1
p q : α × α
⊢ Sym2.mk p = Sym2.mk q ↔ p = q ∨ p = q.swap

Tactic:
cases p

Result:
case mk
α : Type u_1
q : α × α
fst✝ snd✝ : α
⊢ s(fst✝, snd✝) = Sym2.mk q ↔ (fst✝, snd✝) = q ∨ (fst✝, snd✝) = q.swap

Proof state:
case mk
α : Type u_1
q : α × α
fst✝ snd✝ : α
⊢ s(fst✝, snd✝) = Sym2.mk q ↔ (fst✝, snd✝) = q ∨ (fst✝, snd✝) = q.swap

Tactic:
cases q

Result:
case mk.mk
α : Type u_1
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ s(fst✝¹, snd✝¹) = s(fst✝, snd✝) ↔ (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = (fst✝, snd✝).swap

Proof state:
case mk.mk
α : Type u_1
fst✝¹ snd✝¹ fst✝ snd✝ : α
⊢ s(fst✝¹, snd✝¹) = s(fst✝, snd✝) ↔ (fst✝¹, snd✝¹) = (fst✝, snd✝) ∨ (fst✝¹, snd✝¹) = (fst✝, snd✝).swap

Tactic:
simp only [eq_iff, Prod.mk.inj_iff, Prod.swap_prod_mk]

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem map_id : map _ (leComap_id A) = id

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
⊢ map (ContinuousMap.id X) ⋯ = id

Tactic:
ext ⟨⟩

Result:
case h.mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)

Proof state:
case h.mk
X : Type u_2
inst✝ : TopologicalSpace X
A : DiscreteQuotient X
x✝ : Quotient A.toSetoid
a✝ : X
⊢ map (ContinuousMap.id X) ⋯ (Quot.mk (⇑A.toSetoid) a✝) = id (Quot.mk (⇑A.toSetoid) a✝)

Tactic:
rfl

Result:
no goals