harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Div.lean
theorem sum_modByMonic_coeff (hq : q.Monic) {n : ℕ} (hn : q.degree ≤ n) :
    (∑ i : Fin n, monomial i ((p %ₘ q).coeff i)) = p %ₘ q

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
⊢ ∑ i : Fin n, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
a✝ : Nontrivial R
⊢ ∑ i : Fin n, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
a✝ : Nontrivial R
⊢ ∑ i : Fin n, (monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q

Tactic:
exact
  (sum_fin (fun i c => monomial i c) (by simp) ((degree_modByMonic_lt _ hq).trans_le hn)).trans
    (sum_monomial_eq _)

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.Monic
n : ℕ
hn : q.degree ≤ ↑n
a✝ : Nontrivial R
⊢ ∀ (i : ℕ), (fun i c => (monomial i) c) i 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem limsSup_top : limsSup (⊤ : Filter α) = ⊤ :=
  top_unique <| le_sInf <| by simpa [eq_univ_iff_forall] using fun b hb => top_unique <| hb _

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a}, ⊤ ≤ b

Tactic:
simpa [eq_univ_iff_forall] using fun b hb => top_unique <| hb _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem iSup_lt_ord {ι} {f : ι → Ordinal} {c : Ordinal} (hι : #ι < c.cof) :
    (∀ i, f i < c) → iSup f < c :=
  iSup_lt_ord_lift (by rwa [(#ι).lift_id])

Proof state:
ι : Type u_1
f : ι → Ordinal.{u_1}
c : Ordinal.{u_1}
hι : #ι < c.cof
⊢ Cardinal.lift.{?u.28669, u_1} #ι < c.cof

Tactic:
rwa [(#ι).lift_id]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_lt_one_div (h1 : 0 < a) (h2 : a < 1) : 1 < 1 / a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h1 : 0 < a
h2 : a < 1
⊢ 1 < 1 / a

Tactic:
rwa [lt_one_div (@zero_lt_one α _ _ _ _ _) h1, one_div_one]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem supports_union {K₁ K₂ S} : Supports (K₁ ∪ K₂) S ↔ Supports K₁ S ∧ Supports K₂ S

Proof state:
K₁ K₂ S : Finset Λ'
⊢ Supports (K₁ ∪ K₂) S ↔ Supports K₁ S ∧ Supports K₂ S

Tactic:
simp [Supports, or_imp, forall_and]

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toList_toFinset [DecidableEq α] (s : Finset α) : s.toList.toFinset = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.toList.toFinset = s

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.toList.toFinset ↔ a✝ ∈ s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ s.toList.toFinset ↔ a✝ ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_roots' (p : R[X]) : Multiset.card p.roots ≤ natDegree p

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
exact WithBot.coe_le_coe.1 (le_trans (card_roots hp0) (le_of_eq <| degree_eq_natDegree hp0))

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots.card ≤ p.natDegree

Tactic:
by_cases hp0 : p = 0

Result:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p = 0
⊢ p.roots.card ≤ p.natDegree

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : ¬p = 0
⊢ p.roots.card ≤ p.natDegree

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p = 0
⊢ p.roots.card ≤ p.natDegree

Tactic:
simp [hp0]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_finset_sum_index [AddCommMonoid M] [CommMonoid N] {s : Finset ι} {g : ι → α →₀ M}
    {h : α → M → N} (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (∏ i ∈ s, (g i).prod h) = (∑ i ∈ s, g i).prod h :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]

Proof state:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : CommMonoid N
s✝ : Finset ι
g : ι → α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
a : ι
s : Finset ι
has : a ∉ s
ih : ∏ i ∈ s, (g i).prod h = (∑ i ∈ s, g i).prod h
⊢ ∏ i ∈ Finset.cons a s has, (g i).prod h = (∑ i ∈ Finset.cons a s has, g i).prod h

Tactic:
rw [prod_cons, ih, sum_cons, prod_add_index' h_zero h_add]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem insert_iUnion [Nonempty ι] (x : β) (t : ι → Set β) :
    insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Proof state:
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
x : β
t : ι → Set β
⊢ insert x (⋃ i, t i) = ⋃ i, insert x (t i)

Tactic:
simp_rw [← union_singleton, iUnion_union]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_Ici_atTop [Preorder α] [IsDirected α (· ≤ ·)]
    {a : α} {f : β → Ici a} {l : Filter β} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l atTop

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
a : α
f : β → ↑(Ici a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l atTop

Tactic:
rw [atTop_Ici_eq, tendsto_comap_iff, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem coe_join : ∀ L : List (List α), join (L.map ((↑) : List α → Multiset α) :
    Multiset (Multiset α)) = L.flatten
  | [] => rfl
  | l :: L => by
      exact congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)

Proof state:
α : Type u_1
l : List α
L : List (List α)
⊢ (↑(List.map ofList (l :: L))).join = ↑(l :: L).flatten

Tactic:
exact congr_arg (fun s : Multiset α => ↑l + s) (coe_join L)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_iff {o} : IsLimit o ↔ o ≠ 0 ∧ IsSuccPrelimit o

Proof state:
o : Ordinal.{u_4}
⊢ o.IsLimit ↔ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
simp [IsLimit, IsSuccLimit]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc (attr := simp)]
lemma whiskerLeft_μ_δ (X Y : C) (T : D) : T ◁ μ F X Y ≫ T ◁ δ F X Y = 𝟙 _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ T ◁ μ F X Y ≫ T ◁ δ F X Y = 𝟙 (T ⊗ F.obj X ⊗ F.obj Y)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_id]

Result:
no goals
-- Mathlib/RingTheory/IntegralDomain.lean
theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type*} [CommSemiring R] [IsDomain R]
    [GCDMonoid R] [Subsingleton Rˣ] {a b c : R} {n : ℕ} (cp : IsCoprime a b) (h : a * b = c ^ n) :
    ∃ d : R, a = d ^ n

Proof state:
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ GCDMonoid.gcd a b ∣ 1

Tactic:
obtain ⟨x, y, hxy⟩ := cp

Result:
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1

Proof state:
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b

Tactic:
exact  dvd_add (dvd_mul_of_dvd_right (GCDMonoid.gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (GCDMonoid.gcd_dvd_right _ _) _)

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1

Tactic:
rw [← hxy]

Result:
case intro.intro
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b

Proof state:
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ ∃ d, a = d ^ n

Tactic:
refine exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h

Result:
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Subsingleton Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ GCDMonoid.gcd a b ∣ 1
-- Mathlib/Algebra/Ring/Equiv.lean
theorem symm_toRingHom_comp_toRingHom (e : R ≃+* S) :
    e.symm.toRingHom.comp e.toRingHom = RingHom.id _

Proof state:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
x✝ : R
⊢ (e.symm.toRingHom.comp e.toRingHom) x✝ = (RingHom.id R) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
⊢ e.symm.toRingHom.comp e.toRingHom = RingHom.id R

Tactic:
ext

Result:
case a
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
e : R ≃+* S
x✝ : R
⊢ (e.symm.toRingHom.comp e.toRingHom) x✝ = (RingHom.id R) x✝
-- Mathlib/Data/Complex/Trigonometric.lean
theorem abs_sin_le_one : |sin x| ≤ 1 :=
  abs_le_one_iff_mul_self_le_one.2 <| by simp only [← sq, sin_sq_le_one]

Proof state:
x : ℝ
⊢ sin x * sin x ≤ 1

Tactic:
simp only [← sq, sin_sq_le_one]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem iUnion_Icc_right (a : α) : ⋃ b, Icc a b = Ici a

Proof state:
α : Type v
inst✝ : Preorder α
a : α
⊢ ⋃ b, Icc a b = Ici a

Tactic:
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic, inter_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_eq_default_of_contains_eq_false [EquivBEq α] [LawfulHashable α] [Inhabited α]
    (h : m.WF) {a : α} :
    m.contains a = false → m.getKey! a = default

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.WF
a : α
⊢ m.contains a = false → m.getKey! a = default

Tactic:
simp_to_raw using Raw₀.getKey!_eq_default

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
    (Q₁.tmul Q₂).associated = BilinForm.tmul Q₁.associated Q₂.associated

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = BilinForm.tmul (associated Q₁) (associated Q₂)

Tactic:
rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul,
  ← QuadraticMap.associated_tmul Q₁ Q₂]

Result:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = ↑(AlgebraTensorModule.rid R A A).congrRight₂ (associated (QuadraticMap.tmul Q₁ Q₂))

Proof state:
R : Type uR
A : Type uA
M₁ : Type uM₁
M₂ : Type uM₂
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : AddCommGroup M₁
inst✝⁸ : AddCommGroup M₂
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M₁
inst✝⁵ : Module A M₁
inst✝⁴ : SMulCommClass R A M₁
inst✝³ : IsScalarTower R A M₁
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q₁ : QuadraticForm A M₁
Q₂ : QuadraticForm R M₂
⊢ associated (Q₁.tmul Q₂) = ↑(AlgebraTensorModule.rid R A A).congrRight₂ (associated (QuadraticMap.tmul Q₁ Q₂))

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem addNeg_addPos_eq_both (assignment : Assignment) :
    addNegAssignment (addPosAssignment assignment) = both

Proof state:
assignment : Assignment
⊢ assignment.addPosAssignment.addNegAssignment = both

Tactic:
cases assignment <;> simp [addNegAssignment, addPosAssignment]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem memberSubfamily_union (a : α) (𝒜 ℬ : Finset (Finset α)) :
    (𝒜 ∪ ℬ).memberSubfamily a = 𝒜.memberSubfamily a ∪ ℬ.memberSubfamily a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∪ ℬ) = memberSubfamily a 𝒜 ∪ memberSubfamily a ℬ

Tactic:
simp_rw [memberSubfamily, filter_union, image_union]

Result:
no goals
-- Mathlib/Data/Finset/Piecewise.lean
@[simp]
lemma piecewise_eq_of_not_mem {i : ι} (hi : i ∉ s) : s.piecewise f g i = g i

Proof state:
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝ : (j : ι) → Decidable (j ∈ s)
i : ι
hi : i ∉ s
⊢ s.piecewise f g i = g i

Tactic:
simp [piecewise, hi]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive (attr := simp) nnnorm_norm]
lemma nnnorm_norm' (x : E) : ‖‖x‖‖₊ = ‖x‖₊

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
x : E
⊢ ‖‖x‖‖₊ = ‖x‖₊

Tactic:
simp [nnnorm]

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem InfPrime.ne_top (ha : InfPrime a) : a ≠ ⊤

Proof state:
α : Type u_2
inst✝¹ : SemilatticeInf α
a : α
inst✝ : OrderTop α
ha : InfPrime a
⊢ a ≠ ⊤

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfPrime ⊤
⊢ False

Proof state:
α : Type u_2
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
ha : InfPrime ⊤
⊢ False

Tactic:
exact not_infPrime_top ha

Result:
no goals
-- Mathlib/Logic/Function/Conjugate.lean
theorem isIdempotent_left [Std.IdempotentOp gb] (h : Semiconj₂ f ga gb) (h_inj : Injective f) :
    Std.IdempotentOp ga :=
  ⟨fun x ↦ h_inj <| by rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α → α
gb : β → β → β
inst✝ : Std.IdempotentOp gb
h : Semiconj₂ f ga gb
h_inj : Injective f
x : α
⊢ f (ga x x) = f x

Tactic:
rw [h.eq, Std.IdempotentOp.idempotent (op := gb)]

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem primaryComponent.disjoint {p' : ℕ} [hp' : Fact p'.Prime] (hne : p ≠ p') :
    Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p') :=
  Submonoid.disjoint_def.mpr <| by
    rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩
    · rwa [pow_zero, orderOf_eq_one_iff] at hn
    · exact
        absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne

Proof state:
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
⊢ ∀ {x : G}, x ∈ primaryComponent G p → x ∈ primaryComponent G p' → x = 1

Tactic:
rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩

Result:
case intro.zero.intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hn : orderOf g = p ^ 0
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1

case intro.succ.intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ (n + 1)
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1

Proof state:
case intro.succ.intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
n : ℕ
hn : orderOf g = p ^ (n + 1)
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1

Tactic:
exact
  absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne

Result:
no goals

Proof state:
case intro.zero.intro
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hn : orderOf g = p ^ 0
n' : ℕ
hn' : orderOf g = p' ^ n'
⊢ g = 1

Tactic:
rwa [pow_zero, orderOf_eq_one_iff] at hn

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
@[reassoc (attr := simp)]
lemma inr_φ_fst : biprod.inr ≫ φ f g ≫ biprod.fst = - 𝟙 Y

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ biprod.inr ≫ φ f g ≫ biprod.fst = -𝟙 Y

Tactic:
simp [φ]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
@[simp]
lemma cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v (p : ℤ) :
    (cocycleOfDegreewiseSplit _ (triangleRotateShortComplexSplitting φ)).1.v p _ rfl =
      -φ.f _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (↑(cocycleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ))).v p (p + 1) ⋯ =
    -φ.f (p + { as := 1 }.as)

Tactic:
simp [cocycleOfDegreewiseSplit, d_snd_v φ p (p + 1) rfl]

Result:
no goals
-- Mathlib/Data/Finset/Sym.lean
theorem mem_sym2_iff {m : Sym2 α} : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s

Proof state:
α : Type u_1
s : Finset α
m : Sym2 α
⊢ m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s

Tactic:
rw [mem_mk, sym2_val, Multiset.mem_sym2_iff]

Result:
α : Type u_1
s : Finset α
m : Sym2 α
⊢ (∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s

Proof state:
α : Type u_1
s : Finset α
m : Sym2 α
⊢ (∀ y ∈ m, y ∈ s.val) ↔ ∀ a ∈ m, a ∈ s

Tactic:
simp only [mem_val]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem colimitIsoColimitCurryCompColim_ι_ι_inv {j} {k} :
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫
      (colimitIsoColimitCurryCompColim G).inv  = colimit.ι _ (j, k)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_6, u_1} J
inst✝³ : Category.{u_5, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv =
    colimit.ι G (j, k)

Tactic:
simp [colimitIsoColimitCurryCompColim, Trans.simple, colimitUncurryIsoColimitCompColim]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem Pi.reindex_inv_π (b : β) : (Pi.reindex ε f).inv ≫ Pi.π (f ∘ ε) b = Pi.π f (ε b)

Proof state:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (reindex ε f).inv ≫ π (f ∘ ⇑ε) b = π f (ε b)

Tactic:
simp [Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdropWhile_concat_pos (x : α) (h : p x) : rdropWhile p (l ++ [x]) = rdropWhile p l

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
h : p x = true
⊢ rdropWhile p (l ++ [x]) = rdropWhile p l

Tactic:
rw [rdropWhile_concat, if_pos h]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_div_iff_left (a : α) : a / b ≤ a / c ↔ c ≤ b

Proof state:
α : Type u
inst✝³ : Group α
inst✝² : LE α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
b c a : α
⊢ a / b ≤ a / c ↔ c ≤ b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
  inv_mul_cancel_left, inv_le_inv_iff]

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem min [LinearOrder ι] {f : Filtration ι m} {τ π : Ω → ι} (hτ : IsStoppingTime f τ)
    (hπ : IsStoppingTime f π) : IsStoppingTime f fun ω => min (τ ω) (π ω)

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ IsStoppingTime f fun ω => τ ω ⊓ π ω

Tactic:
intro i

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet {ω | (fun ω => τ ω ⊓ π ω) ω ≤ i}

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet ({a | τ a ≤ i} ∪ {a | π a ≤ i})

Tactic:
exact (hτ i).union (hπ i)

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet {ω | (fun ω => τ ω ⊓ π ω) ω ≤ i}

Tactic:
simp_rw [min_le_iff, Set.setOf_or]

Result:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
i : ι
⊢ MeasurableSet ({a | τ a ≤ i} ∪ {a | π a ≤ i})
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_inv_iff_mul_lt_one : a < b⁻¹ ↔ a * b < 1 :=
  (mul_lt_mul_iff_right b).symm.trans <| by rw [inv_mul_cancel]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b : α
⊢ a * b < b⁻¹ * b ↔ a * b < 1

Tactic:
rw [inv_mul_cancel]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_ball_pi_fin {n : ℕ} (x : Fin n → ℝ) {r : ℝ} (hr : 0 < r) :
    dimH (Metric.ball x r) = n

Proof state:
n : ℕ
x : Fin n → ℝ
r : ℝ
hr : 0 < r
⊢ dimH (Metric.ball x r) = ↑n

Tactic:
rw [dimH_ball_pi x hr, Fintype.card_fin]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attach_congr {l₁ l₂ : Array α} (h : l₁ = l₂) :
    l₁.attach = l₂.attach.map (fun x => ⟨x.1, h ▸ x.2⟩)

Proof state:
α : Type u_1
l₁ l₂ : Array α
h : l₁ = l₂
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₂.attach

Tactic:
subst h

Result:
α : Type u_1
l₁ : Array α
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₁.attach

Proof state:
α : Type u_1
l₁ : Array α
⊢ l₁.attach = map (fun x => ⟨x.val, ⋯⟩) l₁.attach

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Basic.lean
theorem le_map_div_mul_map_div [Group α] [CommSemigroup β] [LE β] [SubmultiplicativeHomClass F α β]
    (f : F) (a b c : α) : f (a / c) ≤ f (a / b) * f (b / c)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : CommSemigroup β
inst✝¹ : LE β
inst✝ : SubmultiplicativeHomClass F α β
f : F
a b c : α
⊢ f (a / c) ≤ f (a / b) * f (b / c)

Tactic:
simpa only [div_mul_div_cancel] using map_mul_le_mul f (a / b) (b / c)

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
protected lemma exists_nat_gt {n : ℕ∞} (hn : n ≠ ⊤) : ∃ m : ℕ, n < m

Proof state:
case intro.intro
n m : ℕ
hm : n < m
⊢ ∃ m, ↑n < ↑m

Tactic:
exact ⟨m, Nat.cast_lt.2 hm⟩

Result:
no goals

Proof state:
n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ m, n < ↑m

Tactic:
lift n to ℕ using hn

Result:
case intro
n : ℕ
⊢ ∃ m, ↑n < ↑m

Proof state:
case intro
n : ℕ
⊢ ∃ m, ↑n < ↑m

Tactic:
obtain ⟨m, hm⟩ := exists_gt n

Result:
case intro.intro
n m : ℕ
hm : n < m
⊢ ∃ m, ↑n < ↑m
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ediam_range : EMetric.diam (range (f : α → β)) = ratio f * EMetric.diam (univ : Set α)

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ EMetric.diam (range ⇑f) = ↑(ratio f) * EMetric.diam univ

Tactic:
rw [← image_univ]

Result:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ EMetric.diam (⇑f '' univ) = ↑(ratio f) * EMetric.diam univ

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ EMetric.diam (⇑f '' univ) = ↑(ratio f) * EMetric.diam univ

Tactic:
exact ediam_image f univ

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma ne_zero_pow (hn : n ≠ 0) (ha : a ^ n ≠ 0) : a ≠ 0

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a : M₀
n : ℕ
hn : n ≠ 0
ha : a ^ n ≠ 0
⊢ a ≠ 0

Tactic:
rintro rfl

Result:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : 0 ^ n ≠ 0
⊢ False

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : 0 ^ n ≠ 0
⊢ False

Tactic:
exact ha <| zero_pow hn

Result:
no goals