harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem mono (f : α → E) {s t : Set α} (hst : t ⊆ s) : eVariationOn f t ≤ eVariationOn f s

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
⊢ eVariationOn f t ≤ eVariationOn f s

Tactic:
apply iSup_le _

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ eVariationOn f s

Proof state:
case mk.mk.intro
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
n : ℕ
u : ℕ → α
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤ eVariationOn f s

Tactic:
exact sum_le f n hu fun i => hst (ut i)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }),
    ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ eVariationOn f s

Tactic:
rintro ⟨n, ⟨u, hu, ut⟩⟩

Result:
case mk.mk.intro
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s t : Set α
hst : t ⊆ s
n : ℕ
u : ℕ → α
hu : Monotone u
ut : ∀ (i : ℕ), u i ∈ t
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤ eVariationOn f s
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem trop_sum [AddCommMonoid R] (s : Finset S) (f : S → R) :
    trop (∑ i ∈ s, f i) = ∏ i ∈ s, trop (f i)

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map (fun i => trop (f i)) s.val).prod

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod

Tactic:
simp only [Multiset.map_map, Function.comp_apply]

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map (fun i => trop (f i)) s.val).prod

Proof state:
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ trop (∑ i ∈ s, f i) = ∏ i ∈ s, trop (f i)

Tactic:
convert Multiset.trop_sum (s.val.map f)

Result:
case h.e'_3
R : Type u_1
S : Type u_2
inst✝ : AddCommMonoid R
s : Finset S
f : S → R
⊢ ∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem principal_add_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : Principal (· + ·) c.ord

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ Principal (fun x1 x2 => x1 + x2) c.ord

Tactic:
intro a b ha hb

Result:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 => x1 + x2) a b < c.ord

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c

Tactic:
exact add_lt_of_lt hc ha hb

Result:
no goals

Proof state:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a < c.ord
hb : b < c.ord
⊢ (fun x1 x2 => x1 + x2) a b < c.ord

Tactic:
rw [lt_ord, card_add] at *

Result:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a b : Ordinal.{u_1}
ha : a.card < c
hb : b.card < c
⊢ a.card + b.card < c
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/Multiset.lean
lemma prod_pos {s : Multiset R} (h : ∀ a ∈ s, 0 < a) : 0 < s.prod

Proof state:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a✝ : List R
h : ∀ a ∈ a✝, 0 < a
⊢ 0 < a✝.prod

Tactic:
apply List.prod_pos h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
s : Multiset R
h : ∀ a ∈ s, 0 < a
⊢ 0 < s.prod

Tactic:
cases s using Quotient.ind

Result:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a✝ : List R
h : ∀ a ∈ ⟦a✝⟧, 0 < a
⊢ 0 < prod ⟦a✝⟧

Proof state:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a✝ : List R
h : ∀ a ∈ ⟦a✝⟧, 0 < a
⊢ 0 < prod ⟦a✝⟧

Tactic:
simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *

Result:
case a
R : Type u_1
inst✝⁴ : CommMonoidWithZero R
inst✝³ : PartialOrder R
inst✝² : ZeroLEOneClass R
inst✝¹ : PosMulStrictMono R
inst✝ : NeZero 1
a✝ : List R
h : ∀ a ∈ a✝, 0 < a
⊢ 0 < a✝.prod
-- Mathlib/Data/Set/Basic.lean
theorem inter_nonempty_iff_exists_right : (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s

Proof state:
α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x ∈ t, x ∈ s

Tactic:
simp_rw [inter_nonempty, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem not_and (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q)

Proof state:
p q : Prop
⊢ (¬(p ∧ q)) = (¬p ∨ ¬q)

Tactic:
by_cases p <;> by_cases q <;> simp [*]

Result:
no goals
-- Mathlib/Data/PNat/Prime.lean
theorem gcd_comm {m n : ℕ+} : m.gcd n = n.gcd m

Proof state:
case a
m n : ℕ+
⊢ (↑m).gcd ↑n = (↑n).gcd ↑m

Tactic:
apply Nat.gcd_comm

Result:
no goals

Proof state:
m n : ℕ+
⊢ m.gcd n = n.gcd m

Tactic:
apply eq

Result:
case a
m n : ℕ+
⊢ ↑(m.gcd n) = ↑(n.gcd m)

Proof state:
case a
m n : ℕ+
⊢ ↑(m.gcd n) = ↑(n.gcd m)

Tactic:
simp only [gcd_coe]

Result:
case a
m n : ℕ+
⊢ (↑m).gcd ↑n = (↑n).gcd ↑m
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_Ψ₃_le : W.Ψ₃.natDegree ≤ 4

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₃.natDegree ≤ 4

Tactic:
rw [Ψ₃]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).natDegree ≤ 4

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).natDegree ≤ 4

Tactic:
compute_degree

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_inter_eq_iff (hτ : IsStoppingTime f τ) (s : Set Ω) (i : ι) :
    MeasurableSet[hτ.measurableSpace] (s ∩ {ω | τ ω = i}) ↔
      MeasurableSet[f i] (s ∩ {ω | τ ω = i})

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
⊢ ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}

Tactic:
intro j

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
⊢ {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}

Proof state:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
ω : Ω
⊢ τ ω = i → (τ ω ≤ j ↔ i ≤ j)

Tactic:
intro hxi

Result:
case h
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i j : ι
ω : Ω
hxi : τ ω = i
⊢ τ ω ≤ j ↔ i ≤ j

Proof state:
case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : Preorder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
s : Set Ω
i : ι
this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}
h : MeasurableSet (s ∩ {ω | τ ω = i} ∩ {ω | τ ω ≤ i})
⊢ MeasurableSet (s ∩ {ω | τ ω = i})

Tactic:
simpa only [Set.inter_assoc, this, le_refl, Set.setOf_true, Set.inter_univ] using h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem natDegree_derivative_lt {p : R[X]} (hp : p.natDegree ≠ 0) :
    p.derivative.natDegree < p.natDegree

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
rw [natDegree_lt_natDegree_iff hp']

Result:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).degree < p.degree

Proof state:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ 0 < p.natDegree

Tactic:
exact hp.bot_lt

Result:
no goals

Proof state:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
rw [hp', Polynomial.natDegree_zero]

Result:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ 0 < p.natDegree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Tactic:
rcases eq_or_ne (derivative p) 0 with hp' | hp'

Result:
case inl
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p = 0
⊢ (derivative p).natDegree < p.natDegree

case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).natDegree < p.natDegree

Proof state:
case inr
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.natDegree ≠ 0
hp' : derivative p ≠ 0
⊢ (derivative p).degree < p.degree

Tactic:
exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathConnectedSpace_iff_eq : PathConnectedSpace X ↔ ∃ x : X, pathComponent x = univ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ PathConnectedSpace X ↔ ∃ x, pathComponent x = univ

Tactic:
simp [pathConnectedSpace_iff_univ, isPathConnected_iff_eq]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_div_tan_angle_sub_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Tactic:
rw [sub_eq_add_neg, ← norm_neg, norm_div_tan_angle_add_of_inner_eq_zero h h0]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖

Tactic:
rw [← neg_ne_zero] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem isNoetherian_of_finite_isArtinian {R} [CommRing R] [Module R M]
    [Module.Finite R M] [IsArtinian R M] : IsNoetherian R M

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
⊢ IsNoetherian R (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))

Tactic:
let e (I : Ideal R) : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨.id _, fun _ _ ↦ rfl⟩

Result:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian R (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))
-- Mathlib/NumberTheory/Divisors.lean
theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1 ↔ n.Prime

Proof state:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ sum_singleton _ _⟩

Result:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ (n✝ + 1 + 1).properDivisors = {1}

Proof state:
case zero

⊢ ∑ x ∈ properDivisors 0, x = 1 ↔ Prime 0

Tactic:
simp [Nat.not_prime_zero]

Result:
no goals

Proof state:
case succ.zero

⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ↔ Prime (0 + 1)

Tactic:
simp [Nat.not_prime_one]

Result:
no goals

Proof state:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Tactic:
rw [← properDivisors_eq_singleton_one_iff_prime]

Result:
case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ (n✝ + 1 + 1).properDivisors = {1}

Proof state:
n : ℕ
⊢ ∑ x ∈ n.properDivisors, x = 1 ↔ Prime n

Tactic:
rcases n with - | n

Result:
case zero

⊢ ∑ x ∈ properDivisors 0, x = 1 ↔ Prime 0

case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)

Proof state:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ (n✝ + 1 + 1).properDivisors = {1}

Tactic:
rw [@eq_comm (Finset ℕ) _ _]

Result:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ {1} = (n✝ + 1 + 1).properDivisors

Proof state:
case succ
n : ℕ
⊢ ∑ x ∈ (n + 1).properDivisors, x = 1 ↔ Prime (n + 1)

Tactic:
cases n

Result:
case succ.zero

⊢ ∑ x ∈ (0 + 1).properDivisors, x = 1 ↔ Prime (0 + 1)

case succ.succ
n✝ : ℕ
⊢ ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1 ↔ Prime (n✝ + 1 + 1)

Proof state:
case succ.succ
n✝ : ℕ
h : ∑ x ∈ (n✝ + 1 + 1).properDivisors, x = 1
⊢ {1} = (n✝ + 1 + 1).properDivisors

Tactic:
apply
  eq_properDivisors_of_subset_of_sum_eq_sum
    (singleton_subset_iff.2
      (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
    ((sum_singleton _ _).trans h.symm)

Result:
no goals
-- Mathlib/Analysis/Analytic/Composition.lean
theorem compPartialSumTarget_tendsto_atTop :
    Tendsto (fun N => compPartialSumTarget 0 N N) atTop atTop

Proof state:
⊢ Tendsto (fun N => compPartialSumTarget 0 N N) atTop atTop

Tactic:
apply Tendsto.comp compPartialSumTarget_tendsto_prod_atTop tendsto_atTop_diagonal

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem independent_of_coprime_order
    (hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y)
    [Finite ι] [∀ i, Fintype (H i)]
    (hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
    iSupIndep H

Proof state:
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype ↥(H i)
hcoprime : Pairwise fun i j => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))
⊢ iSupIndep H

Tactic:
simpa using
  MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype)
    (commute_subtype_of_commute hcomm) hcoprime

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
theorem isZero_of_subsingleton (V : SemiNormedGrp) [Subsingleton V] : Limits.IsZero V

Proof state:
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
⊢ Limits.IsZero V

Tactic:
refine ⟨fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩

Result:
case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
⊢ f = default

case refine_2
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
⊢ f = default

Proof state:
case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
⊢ f = default

Tactic:
ext x

Result:
case refine_1.hf.H
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
case refine_1.hf.H
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
simp only [this, map_zero]

Result:
no goals

Proof state:
case refine_1.hf.H
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
have : x = 0 := Subsingleton.elim _ _

Result:
case refine_1.hf.H
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
case refine_2.hf.H
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
x✝ : X.carrier
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Tactic:
apply Subsingleton.elim

Result:
no goals

Proof state:
case refine_2
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
⊢ f = default

Tactic:
ext

Result:
case refine_2.hf.H
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
x✝ : X.carrier
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝
-- Mathlib/Data/Set/NAry.lean
lemma forall_mem_image2 {p : γ → Prop} :
    (∀ z ∈ image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
p : γ → Prop
⊢ (∀ z ∈ image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
lemma finSuccAboveOrderIso_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
    (finSuccAboveOrderIso (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2)

Proof state:
n : ℕ
x : { x // x ≠ last n }
⊢ (finSuccAboveOrderIso (last n)).symm x = (↑x).castLT ⋯

Tactic:
rw [← Option.some_inj]

Result:
n : ℕ
x : { x // x ≠ last n }
⊢ some ((finSuccAboveOrderIso (last n)).symm x) = some ((↑x).castLT ⋯)

Proof state:
n : ℕ
x : { x // x ≠ last n }
⊢ some ((finSuccAboveOrderIso (last n)).symm x) = some ((↑x).castLT ⋯)

Tactic:
simp [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]

Result:
no goals
-- Mathlib/Control/Fix.lean
theorem fix_def' {x : α} (h' : ¬∃ i, (Fix.approx f i x).Dom) : Part.fix f x = none

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ Part.fix f x = none

Tactic:
dsimp [Part.fix]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ (assert (∃ i, (Fix.approx f i x).Dom) fun h => ⋯.fix (fixAux f) Upto.zero x) = none

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ¬∃ i, (Fix.approx f i x).Dom
⊢ (assert (∃ i, (Fix.approx f i x).Dom) fun h => ⋯.fix (fixAux f) Upto.zero x) = none

Tactic:
rw [assert_neg h']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_push_eq (a : Vector α n) (x : α) : (a.push x)[n] = x

Proof state:
case mk
α : Type u_1
x : α
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.push x)[a.size] = x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
x : α
⊢ (a.push x)[n] = x

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
x : α
a : Array α
⊢ ({ toArray := a, size_toArray := ⋯ }.push x)[a.size] = x
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_same {i : ι} {f : Π₀ i, β i} : (f.erase i) i = 0

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

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma pairing_one_four_iff' (h2 : IsSMulRegular R (2 : R)) :
    P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = (2 : R) • P.root i

Proof state:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ P.pairing i j = 1 ∧ P.pairing j i = 4

Tactic:
rw [pairing, pairing, h]

Result:
case refine_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
i j : ι
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : NoZeroSMulDivisors R N
h2 : IsSMulRegular R 2
_i✝ : NoZeroSMulDivisors ℤ M
_i : NoZeroSMulDivisors ℤ N
h : P.coroot i = 2 • P.coroot j
⊢ (P.root' i) (P.coroot j) = 1 ∧ (P.root' j) (2 • P.coroot j) = 4
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertEntry [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
    {v : β} : getValue? a (insertEntry k v l) = if k == a then some v else getValue? a l

Proof state:
case true
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
⊢ getValue? a (insertEntry k v l) = if true = true then some v else getValue? a l

Tactic:
simp [getValue?_insertEntry_of_beq h, h]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
⊢ getValue? a (insertEntry k v l) = if (k == a) = true then some v else getValue? a l

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
⊢ getValue? a (insertEntry k v l) = if false = true then some v else getValue? a l

case true
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
⊢ getValue? a (insertEntry k v l) = if true = true then some v else getValue? a l

Proof state:
case false
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = false
⊢ getValue? a (insertEntry k v l) = if false = true then some v else getValue? a l

Tactic:
simp [getValue?_insertEntry_of_false h, h]

Result:
no goals