harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Interval.lean
theorem Ico_eq_image_ssubsets (h : s ⊆ t) : Ico s t = (t \ s).ssubsets.image (s ∪ ·)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
constructor

Result:
case h.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t → ∃ a ⊂ t \ s, s ∪ a = u

case h.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a ⊂ t \ s, s ∪ a = u) → s ≤ u ∧ u < t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Ico s t ↔ u ∈ image (fun x => s ∪ x) (t \ s).ssubsets

Tactic:
simp_rw [mem_Ico, mem_image, mem_ssubsets]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t ↔ ∃ a ⊂ t \ s, s ∪ a = u

Proof state:
case h.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊂ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v < t

Tactic:
exact ⟨le_sup_left, sup_lt_of_lt_sdiff_left hv h⟩

Result:
no goals

Proof state:
case h.mp
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ s ≤ u ∧ u < t → ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
rintro ⟨hs, ht⟩

Result:
case h.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u < t
⊢ ∃ a ⊂ t \ s, s ∪ a = u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
⊢ Ico s t = image (fun x => s ∪ x) (t \ s).ssubsets

Tactic:
ext u

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ u ∈ Ico s t ↔ u ∈ image (fun x => s ∪ x) (t \ s).ssubsets

Proof state:
case h.mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
⊢ (∃ a ⊂ t \ s, s ∪ a = u) → s ≤ u ∧ u < t

Tactic:
rintro ⟨v, hv, rfl⟩

Result:
case h.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
v : Finset α
hv : v ⊂ t \ s
⊢ s ≤ s ∪ v ∧ s ∪ v < t

Proof state:
case h.mp.intro
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
h : s ⊆ t
u : Finset α
hs : s ≤ u
ht : u < t
⊢ ∃ a ⊂ t \ s, s ∪ a = u

Tactic:
exact ⟨u \ s, sdiff_lt_sdiff_right ht hs, sup_sdiff_cancel_right hs⟩

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable' [Algebra.IsSeparable F E] (a : E)
    (q : ℕ) [ExpChar F q] (n : ℕ) : F⟮a⟯ = F⟮a ^ q ^ n⟯

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra.IsSeparable F E
a : E
q : ℕ
inst✝ : ExpChar F q
n : ℕ
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
haveI := Algebra.isSeparable_tower_bot_of_isSeparable F F⟮a⟯ E

Result:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra.IsSeparable F E
a : E
q : ℕ
inst✝ : ExpChar F q
n : ℕ
this : Algebra.IsSeparable F ↥F⟮a⟯
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Algebra.IsSeparable F E
a : E
q : ℕ
inst✝ : ExpChar F q
n : ℕ
this : Algebra.IsSeparable F ↥F⟮a⟯
⊢ F⟮a⟯ = F⟮a ^ q ^ n⟯

Tactic:
simpa using adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable F E {a} q n

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem le_self_mul_one_div {I : FractionalIdeal R₁⁰ K} (hI : I ≤ (1 : FractionalIdeal R₁⁰ K)) :
    I ≤ I * (1 / I)

Proof state:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)

Tactic:
rw [← coe_le_coe, coe_one] at hI

Result:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : ↑I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)

Proof state:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ I ≤ I * (1 / I)

Tactic:
rw [← coe_le_coe, coe_mul, coe_div hI_nz, coe_one]

Result:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)

Proof state:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ I ≤ I * (1 / I)

Tactic:
rw [hI_nz, div_zero, mul_zero]

Result:
no goals

Proof state:
case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : ↑I ≤ 1
hI_nz : ¬I = 0
⊢ ↑I ≤ ↑I * (1 / ↑I)

Tactic:
exact Submodule.le_self_mul_one_div hI

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
⊢ I ≤ I * (1 / I)

Tactic:
by_cases hI_nz : I = 0

Result:
case pos
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : I = 0
⊢ I ≤ I * (1 / I)

case neg
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I : FractionalIdeal R₁⁰ K
hI : I ≤ 1
hI_nz : ¬I = 0
⊢ I ≤ I * (1 / I)
-- Mathlib/Algebra/Order/Group/Unbundled/Abs.lean
@[to_additive]
lemma mabs_mabs_div_mabs_le (a b : α) : |(|a|ₘ / |b|ₘ)|ₘ ≤ |a / b|ₘ

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs a / mabs b ≤ mabs (a / b) ∧ (mabs a / mabs b)⁻¹ ≤ mabs (a / b)

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs a / mabs b ≤ mabs (a / b)

case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (mabs a / mabs b)⁻¹ ≤ mabs (a / b)

Proof state:
case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs a / mabs b ≤ mabs (a / b)

Tactic:
apply div_le_iff_le_mul.2

Result:
case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs a ≤ mabs (a / b) * mabs b

Proof state:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs b ≤ mabs (b / a) * mabs a

Tactic:
convert mabs_mul_le (b / a) a

Result:
case h.e'_3.h.e'_4
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ b = b / a * a

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs (mabs a / mabs b) ≤ mabs (a / b)

Tactic:
rw [mabs, sup_le_iff]

Result:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs a / mabs b ≤ mabs (a / b) ∧ (mabs a / mabs b)⁻¹ ≤ mabs (a / b)

Proof state:
case h.e'_3.h.e'_4
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ b = b / a * a

Tactic:
rw [div_mul_cancel]

Result:
no goals

Proof state:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ (mabs a / mabs b)⁻¹ ≤ mabs (a / b)

Tactic:
rw [div_eq_mul_inv, mul_inv_rev, inv_inv, mul_inv_le_iff_le_mul, mabs_div_comm]

Result:
case right
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs b ≤ mabs (b / a) * mabs a

Proof state:
case left
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ mabs a ≤ mabs (a / b) * mabs b

Tactic:
convert mabs_mul_le (a / b) b

Result:
case h.e'_3.h.e'_4
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a = a / b * b

Proof state:
case h.e'_3.h.e'_4
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a = a / b * b

Tactic:
rw [div_mul_cancel]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem linearIndependent_monoidHom (G : Type*) [Monoid G] (L : Type*) [CommRing L]
    [NoZeroDivisors L] : LinearIndependent L (M := G → L) (fun f => f : (G →* L) → G → L)

Proof state:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * i (x * y) - ∑ i ∈ insert a s, a x * (g i * i y) =
    (∑ i ∈ insert a s, g i • ⇑i) (x * y) - a x * (∑ i ∈ insert a s, g i • ⇑i) y

Tactic:
rw [Finset.sum_apply, Finset.sum_apply, Finset.mul_sum]

Result:
G : Type u_6
inst✝² : Monoid G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : NoZeroDivisors L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := DistribMulAction.toMulAction
s✝ : Finset (G →* L)
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
i : G →* L
his : i ∈ s
x y : G
⊢ ∑ i ∈ insert a s, g i * i (x * y) - ∑ i ∈ insert a s, a x * (g i * i y) =
    ∑ c ∈ insert a s, (g c • ⇑c) (x * y) - ∑ i ∈ insert a s, a x * (g i • ⇑i) y
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isConj_of_cycleType_eq {σ τ : Perm α} (h : cycleType σ = cycleType τ) : IsConj σ τ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ σ.support.card ∈ τ.cycleType

Tactic:
simp [← h, hc.cycleType]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : cycleType 1 = τ.cycleType
⊢ IsConj 1 τ

Tactic:
rw [cycleType_one, eq_comm, cycleType_eq_zero] at h

Result:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
τ : Perm α
h : τ = 1
⊢ IsConj 1 τ

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ IsConj σ τ

Tactic:
apply hσ.isConj hτ

Result:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ σ.support.card = τ.support.card

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : σ.cycleType.card = 1
⊢ IsConj σ τ

Tactic:
rw [h, card_cycleType_eq_one] at hτ

Result:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : σ.cycleType = τ.cycleType
hτ : τ.IsCycle
⊢ IsConj σ τ
-- Mathlib/GroupTheory/CoprodI.lean
theorem prod_smul (m) : ∀ w : Word M, prod (m • w) = m * prod w

Proof state:
case h_one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ ∀ (w : Word M), (1 • w).prod = 1 * w.prod

Tactic:
intro

Result:
case h_one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w✝ : Word M
⊢ (1 • w✝).prod = 1 * w✝.prod

Proof state:
case h_of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
⊢ ∀ (w : Word M), (of m✝ • w).prod = of m✝ * w.prod

Tactic:
intros

Result:
case h_of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ (of m✝ • w✝).prod = of m✝ * w✝.prod

Proof state:
case h_one
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w✝ : Word M
⊢ (1 • w✝).prod = 1 * w✝.prod

Tactic:
rw [one_smul, one_mul]

Result:
no goals

Proof state:
case h_mul
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod = x * w.prod
hy : ∀ (w : Word M), (y • w).prod = y * w.prod
w : Word M
⊢ ((x * y) • w).prod = x * y * w.prod

Tactic:
rw [mul_smul, hx, hy, mul_assoc]

Result:
no goals

Proof state:
case h_mul
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod = x * w.prod
hy : ∀ (w : Word M), (y • w).prod = y * w.prod
⊢ ∀ (w : Word M), ((x * y) • w).prod = x * y * w.prod

Tactic:
intro w

Result:
case h_mul
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
x y : CoprodI M
hx : ∀ (w : Word M), (x • w).prod = x * w.prod
hy : ∀ (w : Word M), (y • w).prod = y * w.prod
w : Word M
⊢ ((x * y) • w).prod = x * y * w.prod

Proof state:
case h_of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ (of m✝ • w✝).prod = of m✝ * w✝.prod

Tactic:
rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
  Equiv.symm_apply_apply]

Result:
no goals

Proof state:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ ∀ (w : Word M), (m • w).prod = m * w.prod

Tactic:
induction m using CoprodI.induction_on with
| h_one =>
  intro
  rw [one_smul, one_mul]
| h_of _ =>
  intros
  rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm,
    Equiv.symm_apply_apply]
| h_mul x y hx hy =>
  intro w
  rw [mul_smul, hx, hy, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem const_equiv {x y : β} : const x ≈ const y ↔ x = y :=
  show LimZero _ ↔ _ by rw [← const_sub, const_limZero, sub_eq_zero]

Proof state:
α : Type u_1
β : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
x y : β
⊢ (const x - const y).LimZero ↔ x = y

Tactic:
rw [← const_sub, const_limZero, sub_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Defs.lean
theorem fg_def {N : Submodule R M} : N.FG ↔ ∃ S : Set M, S.Finite ∧ span R S = N :=
  ⟨fun ⟨t, h⟩ => ⟨_, Finset.finite_toSet t, h⟩, by
    rintro ⟨t', h, rfl⟩
    rcases Finite.exists_finset_coe h with ⟨t, rfl⟩
    exact ⟨t, rfl⟩⟩

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t' : Set M
h : t'.Finite
⊢ (span R t').FG

Tactic:
rcases Finite.exists_finset_coe h with ⟨t, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Finset M
h : (↑t).Finite
⊢ (span R ↑t).FG

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t : Finset M
h : (↑t).Finite
⊢ (span R ↑t).FG

Tactic:
exact ⟨t, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) → N.FG

Tactic:
rintro ⟨t', h, rfl⟩

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
t' : Set M
h : t'.Finite
⊢ (span R t').FG
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_eq_conj_mul_self {z : ℂ} : (normSq z : ℂ) = conj z * z

Proof state:
z : ℂ
⊢ ↑(normSq z) = (starRingEnd ℂ) z * z

Tactic:
ext <;> simp [normSq, mul_comm, ofReal]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/BinaryProducts.lean
/-- If the product comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
lemma PreservesLimitPair.of_iso_prod_comparison [i : IsIso (prodComparison G X Y)] :
    PreservesLimit (pair X Y) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (G.mapCone (BinaryFan.mk prod.fst prod.snd))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (BinaryFan.mk (G.map prod.fst) (G.map prod.snd))

Tactic:
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsIso ((limit.isLimit (pair (G.obj X) (G.obj Y))).lift (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsIso ((limit.isLimit (pair (G.obj X) (G.obj Y))).lift (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)))

Tactic:
apply i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (G.mapCone (BinaryFan.mk prod.fst prod.snd))

Tactic:
apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (BinaryFan.mk (G.map prod.fst) (G.map prod.snd))
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma polynomialZ_eq : W'.polynomialZ =
    X 1 ^ 2 + C W'.a₁ * X 0 * X 1 + C (2 * W'.a₃) * X 1 * X 2
      - (C W'.a₂ * X 0 ^ 2 + C (2 * W'.a₄) * X 0 * X 2 + C (3 * W'.a₆) * X 2 ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ W'.polynomialZ =
    X y ^ 2 + C W'.a₁ * X x * X y + C (2 * W'.a₃) * X y * X z -
      (C W'.a₂ * X x ^ 2 + C (2 * W'.a₄) * X x * X z + C (3 * W'.a₆) * X z ^ 2)

Tactic:
rw [polynomialZ, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv z)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    X y ^ 2 + C W'.a₁ * X x * X y + C (2 * W'.a₃) * X y * X z -
      (C W'.a₂ * X x ^ 2 + C (2 * W'.a₄) * X x * X z + C (3 * W'.a₆) * X z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv z)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    X y ^ 2 + C W'.a₁ * X x * X y + C (2 * W'.a₃) * X y * X z -
      (C W'.a₂ * X x ^ 2 + C (2 * W'.a₄) * X x * X z + C (3 * W'.a₆) * X z ^ 2)

Tactic:
pderiv_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * X y ^ (2 - 1) * 0 * X z + X y ^ 2 * 1 +
          (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 1) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 2 + C W'.a₃ * X y * (↑2 * X z ^ (2 - 1) * 1)) -
      (↑3 * X x ^ (3 - 1) * 0 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z + C W'.a₂ * X x ^ 2 * 1) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 2 + C W'.a₄ * X x * (↑2 * X z ^ (2 - 1) * 1)) +
        (0 * X z ^ 3 + C W'.a₆ * (↑3 * X z ^ (3 - 1) * 1))) =
    X y ^ 2 + C W'.a₁ * X x * X y + 2 * C W'.a₃ * X y * X z -
      (C W'.a₂ * X x ^ 2 + 2 * C W'.a₄ * X x * X z + 3 * C W'.a₆ * X z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * X y ^ (2 - 1) * 0 * X z + X y ^ 2 * 1 +
          (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 1) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 2 + C W'.a₃ * X y * (↑2 * X z ^ (2 - 1) * 1)) -
      (↑3 * X x ^ (3 - 1) * 0 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z + C W'.a₂ * X x ^ 2 * 1) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 2 + C W'.a₄ * X x * (↑2 * X z ^ (2 - 1) * 1)) +
        (0 * X z ^ 3 + C W'.a₆ * (↑3 * X z ^ (3 - 1) * 1))) =
    X y ^ 2 + C W'.a₁ * X x * X y + 2 * C W'.a₃ * X y * X z -
      (C W'.a₂ * X x ^ 2 + 2 * C W'.a₄ * X x * X z + 3 * C W'.a₆ * X z ^ 2)

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/QPF/Multivariate/Basic.lean
theorem liftP_iff_of_isUniform (h : q.IsUniform) {α : TypeVec n} (x : F α) (p : ∀ i, α i → Prop) :
    LiftP p x ↔ ∀ (i), ∀ u ∈ supp x i, p i u

Proof state:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ LiftP p x ↔ ∀ (i : Fin2 n), ∀ u ∈ supp x i, p i u

Tactic:
rw [liftP_iff, ← abs_repr x]

Result:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs (repr x)) i, p i u
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem weightedTotalDegree_one (φ : MvPolynomial σ R) :
    weightedTotalDegree (1 : σ → ℕ) φ = φ.totalDegree

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ weightedTotalDegree 1 φ = φ.totalDegree

Tactic:
simp only [totalDegree, weightedTotalDegree, weight, LinearMap.toAddMonoidHom_coe,
  linearCombination, Pi.one_apply, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
  id, Algebra.id.smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem div_congr {R} [DivisionRing R] {a a' b b' c : R} (_ : a = a') (_ : b = b')
    (_ : a' / b' = c) : (a / b : R) = c

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a' b' : R
⊢ a' / b' = a' / b'

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝ : DivisionRing R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' / b' = c
⊢ a / b = c

Tactic:
subst_vars

Result:
R : Type u_2
inst✝ : DivisionRing R
a' b' : R
⊢ a' / b' = a' / b'
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem smulRight_comp [ContinuousMul R₁] {x : M₂} {c : R₁} :
    (smulRight (1 : R₁ →L[R₁] R₁) x).comp (smulRight (1 : R₁ →L[R₁] R₁) c) =
      smulRight (1 : R₁ →L[R₁] R₁) (c • x)

Proof state:
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₂ : Type u_6
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₁ M₂
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₂
inst✝ : ContinuousMul R₁
x : M₂
c : R₁
⊢ (smulRight 1 x).comp (smulRight 1 c) = smulRight 1 (c • x)

Tactic:
ext

Result:
case h
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₂ : Type u_6
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₁ M₂
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₂
inst✝ : ContinuousMul R₁
x : M₂
c : R₁
⊢ ((smulRight 1 x).comp (smulRight 1 c)) 1 = (smulRight 1 (c • x)) 1

Proof state:
case h
R₁ : Type u_1
inst✝⁶ : Semiring R₁
M₂ : Type u_6
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R₁ M₂
inst✝² : TopologicalSpace R₁
inst✝¹ : ContinuousSMul R₁ M₂
inst✝ : ContinuousMul R₁
x : M₂
c : R₁
⊢ ((smulRight 1 x).comp (smulRight 1 c)) 1 = (smulRight 1 (c • x)) 1

Tactic:
simp [mul_smul]

Result:
no goals