harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Pointwise.lean
theorem zero_smul_filter_nonpos : (0 : α) • g ≤ 0

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x => 0 • x) ⁻¹' s ∈ g

Tactic:
convert @univ_mem _ g

Result:
case h.e'_5
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x => 0 • x) ⁻¹' s = univ

Proof state:
case h.e'_5
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x => 0 • x) ⁻¹' s = univ

Tactic:
refine eq_univ_iff_forall.2 fun a => ?_

Result:
case h.e'_5
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x => 0 • x) ⁻¹' s

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
⊢ 0 • g ≤ 0

Tactic:
refine fun s hs => mem_smul_filter.2 ?_

Result:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
⊢ (fun x => 0 • x) ⁻¹' s ∈ g

Proof state:
case h.e'_5
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x => 0 • x) ⁻¹' s

Tactic:
rwa [mem_preimage, zero_smul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_mul_of_domain : (p * q).mirror = p.mirror * q.mirror

Proof state:
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [hq, mul_zero, mirror_zero, mul_zero]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
rw [mul_assoc, ← mul_assoc q.reverse, ← X_pow_mul (p := reverse q)]

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [mirror, mirror, mirror, reverse_mul_of_domain, natTrailingDegree_mul hp hq, pow_add]

Result:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * q.reverse * (X ^ p.natTrailingDegree * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Proof state:
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
rw [hp, zero_mul, mirror_zero, zero_mul]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
hq : ¬q = 0
⊢ p.reverse * (X ^ p.natTrailingDegree * q.reverse * X ^ q.natTrailingDegree) =
    p.reverse * X ^ p.natTrailingDegree * (q.reverse * X ^ q.natTrailingDegree)

Tactic:
repeat' rw [mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
⊢ (p * q).mirror = p.mirror * q.mirror

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : p = 0
⊢ (p * q).mirror = p.mirror * q.mirror

case neg
R : Type u_1
inst✝¹ : Ring R
p q : R[X]
inst✝ : NoZeroDivisors R
hp : ¬p = 0
⊢ (p * q).mirror = p.mirror * q.mirror
-- Mathlib/Topology/MetricSpace/ThickenedIndicator.lean
theorem indicator_le_thickenedIndicatorAux (δ : ℝ) (E : Set α) :
    (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ thickenedIndicatorAux δ E

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ (E.indicator fun x => 1) ≤ thickenedIndicatorAux δ E

Tactic:
intro a

Result:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ E.indicator (fun x => 1) a ≤ thickenedIndicatorAux δ E a

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ E.indicator (fun x => 1) a ≤ thickenedIndicatorAux δ E a

Tactic:
by_cases h : a ∈ E

Result:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∈ E
⊢ E.indicator (fun x => 1) a ≤ thickenedIndicatorAux δ E a

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun x => 1) a ≤ thickenedIndicatorAux δ E a

Proof state:
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∈ E
⊢ E.indicator (fun x => 1) a ≤ thickenedIndicatorAux δ E a

Tactic:
simp only [h, indicator_of_mem, thickenedIndicatorAux_one δ E h, le_refl]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun x => 1) a ≤ thickenedIndicatorAux δ E a

Tactic:
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem degree_eq_one_iff : (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
x : A
this : Nontrivial A
⊢ (Polynomial.aeval ((algebraMap A B) x)) (X - C x) = 0

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ (minpoly A x).degree = 1 ↔ x ∈ (algebraMap A B).range

Tactic:
refine ⟨minpoly.mem_range_of_degree_eq_one _ _, ?_⟩

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ x ∈ (algebraMap A B).range → (minpoly A x).degree = 1

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
x : A
⊢ (minpoly A ((algebraMap A B) x)).degree = 1

Tactic:
haveI := Module.nontrivial A B

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
x : A
this : Nontrivial A
⊢ (minpoly A ((algebraMap A B) x)).degree = 1

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
x : A
this : Nontrivial A
⊢ (minpoly A ((algebraMap A B) x)).degree = 1

Tactic:
exact (degree_X_sub_C x ▸ minpoly.min A (algebraMap A B x) (monic_X_sub_C x) (by simp)).antisymm
  (Nat.WithBot.add_one_le_of_lt <| minpoly.degree_pos isIntegral_algebraMap)

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ x ∈ (algebraMap A B).range → (minpoly A x).degree = 1

Tactic:
rintro ⟨x, rfl⟩

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
x : A
⊢ (minpoly A ((algebraMap A B) x)).degree = 1
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma tensorHom_mem {X₁ X₂ : C} (f : X₁ ⟶ X₂) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂)
    (hf : W f) (hg : W g) : W (f ⊗ g)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ▷ Y₁ ≫ X₂ ◁ g)

Tactic:
exact comp_mem _ _ _ (whiskerRight_mem _ _ hf _) (whiskerLeft_mem _ _ _ hg)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ⊗ g)

Tactic:
rw [tensorHom_def]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝¹ : MonoidalCategory C
inst✝ : W.IsMonoidal
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf : W f
hg : W g
⊢ W (f ▷ Y₁ ≫ X₂ ◁ g)
-- Mathlib/Data/Finset/Insert.lean
theorem eq_singleton_iff_nonempty_unique_mem {s : Finset α} {a : α} :
    s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a

Tactic:
constructor

Result:
case mp
α : Type u_1
s : Finset α
a : α
⊢ s = {a} → s.Nonempty ∧ ∀ x ∈ s, x = a

case mpr
α : Type u_1
s : Finset α
a : α
⊢ (s.Nonempty ∧ ∀ x ∈ s, x = a) → s = {a}

Proof state:
case mpr
α : Type u_1
s : Finset α
a : α
⊢ (s.Nonempty ∧ ∀ x ∈ s, x = a) → s = {a}

Tactic:
rintro ⟨hne, h_uniq⟩

Result:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ s = {a}

Proof state:
case mp
α : Type u_1
s : Finset α
a : α
⊢ s = {a} → s.Nonempty ∧ ∀ x ∈ s, x = a

Tactic:
rintro rfl

Result:
case mp
α : Type u_1
a : α
⊢ {a}.Nonempty ∧ ∀ x ∈ {a}, x = a

Proof state:
case mp
α : Type u_1
a : α
⊢ {a}.Nonempty ∧ ∀ x ∈ {a}, x = a

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ a ∈ s ∧ ∀ x ∈ s, x = a

Tactic:
refine ⟨?_, h_uniq⟩

Result:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ a ∈ s

Proof state:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ a ∈ s

Tactic:
rw [← h_uniq hne.choose hne.choose_spec]

Result:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ Exists.choose hne ∈ s

Proof state:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ s = {a}

Tactic:
rw [eq_singleton_iff_unique_mem]

Result:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ a ∈ s ∧ ∀ x ∈ s, x = a

Proof state:
case mpr.intro
α : Type u_1
s : Finset α
a : α
hne : s.Nonempty
h_uniq : ∀ x ∈ s, x = a
⊢ Exists.choose hne ∈ s

Tactic:
exact hne.choose_spec

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_modEq' (b b' : ℕ) (k : ℕ) (h : b ≡ b' [MOD k]) (L : List ℕ) :
    ofDigits b L ≡ ofDigits b' L [MOD k]

Proof state:
case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k

Tactic:
conv_lhs => rw [Nat.add_mod, Nat.mul_mod, h, ih]

Result:
case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k

Proof state:
b b' k : ℕ
h : b ≡ b' [MOD k]
L : List ℕ
⊢ ofDigits b L ≡ ofDigits b' L [MOD k]

Tactic:
induction' L with d L ih

Result:
case nil
b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]

case cons
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]

Proof state:
case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d % k + b' % k * (ofDigits b' L % k) % k) % k = (d + b' * ofDigits b' L) % k

Tactic:
conv_rhs => rw [Nat.add_mod, Nat.mul_mod]

Result:
no goals

Proof state:
case nil
b b' k : ℕ
h : b ≡ b' [MOD k]
⊢ ofDigits b [] ≡ ofDigits b' [] [MOD k]

Tactic:
rfl

Result:
no goals

Proof state:
case cons
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]

Tactic:
dsimp [Nat.ModEq] at *

Result:
case cons
b b' k : ℕ
h : b % k = b' % k
d : ℕ
L : List ℕ
ih : ofDigits b L % k = ofDigits b' L % k
⊢ (d + b * ofDigits b L) % k = (d + b' * ofDigits b' L) % k

Proof state:
case cons
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ ofDigits b (d :: L) ≡ ofDigits b' (d :: L) [MOD k]

Tactic:
dsimp [ofDigits]

Result:
case cons
b b' k : ℕ
h : b ≡ b' [MOD k]
d : ℕ
L : List ℕ
ih : ofDigits b L ≡ ofDigits b' L [MOD k]
⊢ d + b * ofDigits b L ≡ d + b' * ofDigits b' L [MOD k]
-- Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
theorem biUnion_lt_closedBall (x : α) (r : ℝ) : ⋃ r' < r, closedBall x r' = ball x r

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∈ ball x r

Tactic:
rw [← not_iff_not]

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∉ ball x r

Proof state:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ r', ⋃ (_ : r' < r), closedBall x r' = ball x r

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∈ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∈ ball x r

Proof state:
case h
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), closedBall x r' ↔ x✝ ∉ ball x r

Tactic:
simp [forall_lt_iff_le]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffEdist_self : hausdorffEdist s s = 0

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEdist s s = 0

Tactic:
simp only [hausdorffEdist_def, sup_idem, ENNReal.iSup_eq_zero]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ i ∈ s, infEdist i s = 0

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ ∀ i ∈ s, infEdist i s = 0

Tactic:
exact fun x hx => infEdist_zero_of_mem hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_self_right : ∀ (a b : Bool), ((a && b) && b) = (a && b)

Proof state:
⊢ ∀ (a b : Bool), (a && b && b) = (a && b)

Tactic:
decide

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma subsingleton_iff {n : ℕ} : Subsingleton (ZMod n) ↔ n = 1

Proof state:
n : ℕ
⊢ Subsingleton (ZMod n) ↔ n = 1

Tactic:
constructor

Result:
case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1

case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Proof state:
case mp.succ.zero

⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

Tactic:
simp [ZMod]

Result:
no goals

Proof state:
case mpr

⊢ Subsingleton (ZMod 1)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr
n : ℕ
⊢ n = 1 → Subsingleton (ZMod n)

Tactic:
rintro rfl

Result:
case mpr

⊢ Subsingleton (ZMod 1)

Proof state:
case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Tactic:
simpa [ZMod] using not_subsingleton _

Result:
no goals

Proof state:
case mp
n : ℕ
⊢ Subsingleton (ZMod n) → n = 1

Tactic:
obtain (_ | _ | n) := n

Result:
case mp.zero

⊢ Subsingleton (ZMod 0) → 0 = 1

case mp.succ.zero

⊢ Subsingleton (ZMod (0 + 1)) → 0 + 1 = 1

case mp.succ.succ
n : ℕ
⊢ Subsingleton (ZMod (n + 1 + 1)) → n + 1 + 1 = 1

Proof state:
case mp.zero

⊢ Subsingleton (ZMod 0) → 0 = 1

Tactic:
simpa [ZMod] using not_subsingleton _

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
@[simp, reassoc]
lemma mapBifunctorRightUnitorCofan_inj (j : J) :
    (mapBifunctorRightUnitorCofan F Y e p hp X j).inj ⟨⟨j, 0⟩, hp j⟩ =
      (F.obj (X j)).map (singleObjApplyIso (0 : I) Y).hom ≫ e.hom.app (X j)

Proof state:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_5, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X : GradedObject J D
j : J
⊢ Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) ⟨(j, 0), ⋯⟩ =
    (F.obj (X j)).map (singleObjApplyIso 0 Y).hom ≫ e.hom.app (X j)

Tactic:
simp [mapBifunctorRightUnitorCofan]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedProcess_eq (n : ℕ) : stoppedProcess u τ n = Set.indicator {a | n ≤ τ a} (u n) +
    ∑ i ∈ Finset.range n, Set.indicator {ω | τ ω = i} (u i)

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
⊢ {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i) =
    {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = i}.indicator (u i)

Tactic:
congr with i

Result:
case e_a.e_s.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n i : ℕ
⊢ i ∈ Finset.Iio n ↔ i ∈ Finset.range n

Proof state:
case e_a.e_s.h
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n i : ℕ
⊢ i ∈ Finset.Iio n ↔ i ∈ Finset.range n

Tactic:
rw [Finset.mem_Iio, Finset.mem_range]

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
⊢ stoppedProcess u τ n = {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = i}.indicator (u i)

Tactic:
rw [stoppedProcess_eq'' n]

Result:
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ
inst✝ : AddCommMonoid β
n : ℕ
⊢ {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.Iio n, {ω | τ ω = i}.indicator (u i) =
    {a | n ≤ τ a}.indicator (u n) + ∑ i ∈ Finset.range n, {ω | τ ω = i}.indicator (u i)
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem aux_inj_roots_of_min_poly : Injective (rootsOfMinPolyPiType F E K)

Proof state:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ f = g

Tactic:
suffices (f : E →ₗ[F] K) = (g : E →ₗ[F] K) by rwa [DFunLike.ext'_iff] at this ⊢

Result:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ ↑f = ↑g

Proof state:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
this : ↑f = ↑g
⊢ f = g

Tactic:
rwa [DFunLike.ext'_iff] at this ⊢

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : ∀ (x : ↑(range ⇑(Module.finBasis F E))), rootsOfMinPolyPiType F E K f x = rootsOfMinPolyPiType F E K g x
⊢ ↑f = ↑g

Tactic:
exact LinearMap.ext_on (Module.finBasis F E).span_eq fun e he =>
  Subtype.ext_iff.mp (h ⟨e, he⟩)

Result:
no goals

Proof state:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
⊢ Injective (rootsOfMinPolyPiType F E K)

Tactic:
intro f g h

Result:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ f = g

Proof state:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g
⊢ ↑f = ↑g

Tactic:
rw [funext_iff] at h

Result:
F : Type u_3
E : Type u_4
K : Type u_5
inst✝⁶ : Field F
inst✝⁵ : Ring E
inst✝⁴ : CommRing K
inst✝³ : IsDomain K
inst✝² : Algebra F E
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F E
f g : E →ₐ[F] K
h : ∀ (x : ↑(range ⇑(Module.finBasis F E))), rootsOfMinPolyPiType F E K f x = rootsOfMinPolyPiType F E K g x
⊢ ↑f = ↑g
-- Mathlib/Analysis/Meromorphic/Basic.lean
@[fun_prop]
lemma inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt f⁻¹ x

Proof state:
case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m * f z = (z - x) ^ n * g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
aux1 : f z ≠ 0
⊢ (z - x) ^ (m + 1) * f z = (z - x) ^ (n + 1) * g z

Tactic:
rw [pow_succ', mul_assoc, hfg]

Result:
case h.inr
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x : 𝕜
m : ℕ
hf : AnalyticAt 𝕜 (fun z => (z - x) ^ m • f z) x
h_eq : ¬(fun z => (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
n : ℕ
g : 𝕜 → 𝕜
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (fun z => (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m * f z = (z - x) ^ n * g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
aux1 : f z ≠ 0
⊢ (z - x) * ((z - x) ^ n * g z) = (z - x) ^ (n + 1) * g z
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_rotate (l : List α) (h : Nodup l) (n : ℕ) :
    formPerm (l.rotate n) = formPerm l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
⊢ (l.rotate n).formPerm = l.formPerm

Tactic:
induction n with
| zero => simp
| succ n hn =>
  rw [← rotate_rotate, formPerm_rotate_one, hn]
  rwa [IsRotated.nodup_iff]
  exact IsRotated.forall l n

Result:
no goals

Proof state:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup

Tactic:
rwa [IsRotated.nodup_iff]

Result:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r l

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 0).formPerm = l.formPerm

Tactic:
simp

Result:
no goals

Proof state:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r l

Tactic:
exact IsRotated.forall l n

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate (n + 1)).formPerm = l.formPerm

Tactic:
rw [← rotate_rotate, formPerm_rotate_one, hn]

Result:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_homogeneousComponent (p : ℕ) (d : σ →₀ ℕ) (f : MvPowerSeries σ R) :
    coeff R d (homogeneousComponent p f) =
      if degree d = p then coeff R d f else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ (coeff R d) ((homogeneousComponent p) f) = if (weight fun x => 1) d = p then (coeff R d) f else 0

Tactic:
exact coeff_weightedHomogeneousComponent 1 p d f

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ (coeff R d) ((homogeneousComponent p) f) = if d.degree = p then (coeff R d) f else 0

Tactic:
rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
p : ℕ
d : σ →₀ ℕ
f : MvPowerSeries σ R
⊢ (coeff R d) ((homogeneousComponent p) f) = if (weight fun x => 1) d = p then (coeff R d) f else 0