harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
theorem quaternionGroup_one_isCyclic : IsCyclic (QuaternionGroup 1)

Proof state:
⊢ IsCyclic (QuaternionGroup 1)

Tactic:
apply isCyclic_of_orderOf_eq_card

Result:
case hx

⊢ orderOf ?x = Nat.card (QuaternionGroup 1)

case x

⊢ QuaternionGroup 1

Proof state:
case hx

⊢ orderOf ?x = 4

Tactic:
exact orderOf_xa 0

Result:
no goals

Proof state:
case hx

⊢ orderOf ?x = Nat.card (QuaternionGroup 1)

Tactic:
rw [Nat.card_eq_fintype_card, card, mul_one]

Result:
case hx

⊢ orderOf ?x = 4
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
lemma HasExt.standard : HasExt.{max u v} C

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasExt C

Tactic:
letI := HasDerivedCategory.standard

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (C : Type ?u.37386) → [inst : Category.{?u.37387, ?u.37386} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasExt C

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : (C : Type ?u.37386) → [inst : Category.{?u.37387, ?u.37386} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasExt C

Tactic:
exact hasExt_of_hasDerivedCategory _

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma HomologyData.exact_iff_i_p_zero (h : S.HomologyData) :
    S.Exact ↔ h.left.i ≫ h.right.p = 0

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
eq : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ IsZero h.left.H

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_mono h.iso.hom, id_comp, ← cancel_mono h.right.ι,
  ← cancel_epi h.left.π, eq, zero_comp, comp_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0

Tactic:
haveI := HasHomology.mk' h

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Tactic:
rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero h.left.H

Tactic:
intro eq

Result:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
eq : h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
⊢ IsZero h.left.H

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ IsZero h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ IsZero h.left.H → h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero h.left.H

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0

Tactic:
rw [h.left.exact_iff, ← h.comm]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ IsZero h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ IsZero h.left.H → h.left.π ≫ h.iso.hom ≫ h.right.ι = 0

Tactic:
intro z

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
z : IsZero h.left.H
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem finset_sum_comp {ι : Type*} {s : Finset ι}
    [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃)
    (f : M₁ →SL[σ₁₂] M₂) : (∑ i ∈ s, g i).comp f = ∑ i ∈ s, (g i).comp f

Proof state:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝ : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((∑ i ∈ s, g i).comp f) x✝ = (∑ i ∈ s, (g i).comp f) x✝

Tactic:
simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply]

Result:
no goals

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝ : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
⊢ (∑ i ∈ s, g i).comp f = ∑ i ∈ s, (g i).comp f

Tactic:
ext

Result:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹³ : Semiring R₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R₁ M₁
inst✝³ : Module R₂ M₂
inst✝² : Module R₃ M₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝ : ContinuousAdd M₃
g : ι → M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((∑ i ∈ s, g i).comp f) x✝ = (∑ i ∈ s, (g i).comp f) x✝
-- Mathlib/Analysis/SpecialFunctions/Exponential.lean
theorem Complex.exp_eq_exp_ℂ : Complex.exp = NormedSpace.exp ℂ

Proof state:
⊢ cexp = NormedSpace.exp ℂ

Tactic:
refine funext fun x => ?_

Result:
x : ℂ
⊢ cexp x = NormedSpace.exp ℂ x

Proof state:
x : ℂ
this : CauSeq.IsComplete ℂ norm
⊢ (exp' x).lim = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x

Tactic:
exact tendsto_nhds_unique x.exp'.tendsto_limit (expSeries_div_summable ℝ x).hasSum.tendsto_sum_nat

Result:
no goals

Proof state:
x : ℂ
⊢ (exp' x).lim = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x

Tactic:
have : CauSeq.IsComplete ℂ norm := Complex.instIsComplete

Result:
x : ℂ
this : CauSeq.IsComplete ℂ norm
⊢ (exp' x).lim = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x

Proof state:
x : ℂ
⊢ cexp x = NormedSpace.exp ℂ x

Tactic:
rw [Complex.exp, exp_eq_tsum_div]

Result:
x : ℂ
⊢ (exp' x).lim = (fun x => ∑' (n : ℕ), x ^ n / ↑n !) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_eq_push_iff {xs : Array (Array α)} {ys : Array α} {y : α} :
    xs.flatten = ys.push y ↔
      ∃ (as : Array (Array α)) (bs : Array α) (cs : Array (Array α)),
        xs = as.push (bs.push y) ++ cs ∧ (∀ l, l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs

Proof state:
case of.mk.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h : [y] = c :: cs ++ ds.flatten
⊢ ∃ as_1 bs_1 cs_1,
    (List.map List.toArray (as ++ (bs ++ c :: cs) :: ds)).toArray = as_1.push (bs_1.push y) ++ cs_1 ∧
      (∀ (l : Array α), l ∈ cs_1 → l = #[]) ∧ { toList := as.flatten ++ bs } = as_1.flatten ++ bs_1

Tactic:
rw [List.singleton_eq_append_iff] at h

Result:
case of.mk.mp.inr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
y : α
as : List (List α)
bs : List α
c : α
cs : List α
ds : List (List α)
h : c :: cs = [] ∧ ds.flatten = [y] ∨ c :: cs = [y] ∧ ds.flatten = []
⊢ ∃ as_1 bs_1 cs_1,
    (List.map List.toArray (as ++ (bs ++ c :: cs) :: ds)).toArray = as_1.push (bs_1.push y) ++ cs_1 ∧
      (∀ (l : Array α), l ∈ cs_1 → l = #[]) ∧ { toList := as.flatten ++ bs } = as_1.flatten ++ bs_1
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem map_le_map_iff (f : F) {p p'} : map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_8
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
p p' : Submodule R M
⊢ map f p ≤ map f p' ↔ p ≤ p' ⊔ ker f

Tactic:
rw [map_le_iff_le_comap, Submodule.comap_map_eq]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem le_nhdsAdjoint_iff' {a : α} {f : Filter α} {t : TopologicalSpace α} :
    t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, @nhds α t b = pure b

Proof state:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
classical
simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).le_iff_eq]

Result:
no goals

Proof state:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → 𝓝 b = pure b

Tactic:
simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).le_iff_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
lemma differentiableAt_iff_comp_add_const {a b : 𝕜} :
    DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x ↦ f (x + b)) (a - b)

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (x + b)) (a - b)

Tactic:
simp [differentiableAt_comp_add_const]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem Isometry.norm_map_of_map_one {f : E → F} (hi : Isometry f) (h₁ : f 1 = 1) (x : E) :
    ‖f x‖ = ‖x‖

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
hi : Isometry f
h₁ : f 1 = 1
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
rw [← dist_one_right, ← h₁, hi.dist_eq, dist_one_right]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem support_sdiff_support_subset_support_add [DecidableEq σ] (p q : MvPolynomial σ R) :
    p.support \ q.support ⊆ (p + q).support

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : ¬coeff m p = 0 ∧ coeff m q = 0
⊢ m ∈ (p + q).support

Tactic:
simp [hm.2, hm.1]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : m ∈ p.support \ q.support
⊢ m ∈ (p + q).support

Tactic:
simp only [Classical.not_not, mem_support_iff, Finset.mem_sdiff, Ne] at hm

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : ¬coeff m p = 0 ∧ coeff m q = 0
⊢ m ∈ (p + q).support

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ p.support \ q.support ⊆ (p + q).support

Tactic:
intro m hm

Result:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
m : σ →₀ ℕ
hm : m ∈ p.support \ q.support
⊢ m ∈ (p + q).support
-- Mathlib/Topology/Order.lean
theorem nhds_nhdsAdjoint_same (a : α) (f : Filter α) :
    @nhds α (nhdsAdjoint a f) a = pure a ⊔ f

Proof state:
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f

Tactic:
apply le_antisymm

Result:
case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a ≤ pure a ⊔ f

case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ pure a ⊔ f ≤ 𝓝 a

Proof state:
case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a ≤ pure a ⊔ f

Tactic:
rintro t ⟨hat : a ∈ t, htf : t ∈ f⟩

Result:
case a.intro
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
t : Set α
hat : a ∈ t
htf : t ∈ f
⊢ t ∈ 𝓝 a

Proof state:
case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ pure a ⊔ f ≤ 𝓝 a

Tactic:
exact sup_le (pure_le_nhds _) ((gc_nhds a).le_u_l f)

Result:
no goals

Proof state:
case a.intro
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
t : Set α
hat : a ∈ t
htf : t ∈ f
⊢ t ∈ 𝓝 a

Tactic:
exact IsOpen.mem_nhds (fun _ ↦ htf) hat

Result:
no goals

Proof state:
α : Type u
a : α
f : Filter α
⊢ 𝓝 a = pure a ⊔ f

Tactic:
let _ := nhdsAdjoint a f

Result:
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
⊢ 𝓝 a = pure a ⊔ f
-- Mathlib/SetTheory/Cardinal/Divisibility.lean
theorem nat_coe_dvd_iff : (n : Cardinal) ∣ m ↔ n ∣ m

Proof state:
n m : ℕ
⊢ ↑n ∣ ↑m ↔ n ∣ m

Tactic:
refine ⟨?_, fun ⟨h, ht⟩ => ⟨h, mod_cast ht⟩⟩

Result:
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m

Proof state:
case intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m

Tactic:
rcases this with (h | h | ⟨-, hk'⟩)

Result:
case intro.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m

case intro.inr.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Proof state:
case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Tactic:
lift k to ℕ using hk'

Result:
case intro.inr.inr.intro.intro
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m

Proof state:
n m : ℕ
⊢ ↑n ∣ ↑m → n ∣ m

Tactic:
rintro ⟨k, hk⟩

Result:
case intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
⊢ n ∣ m

Proof state:
case intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
⊢ n ∣ m

Tactic:
have : ↑m < ℵ₀ := nat_lt_aleph0 m

Result:
case intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m

Proof state:
case intro.inr.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Tactic:
simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk

Result:
case intro.inr.inl
n m : ℕ
k : Cardinal.{u_1}
h : k = 0
hk : m = 0
⊢ n ∣ m

case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Proof state:
case intro.inr.inr.intro.intro
n m k : ℕ
hk : ↑m = ↑n * ↑k
⊢ n ∣ m

Tactic:
exact ⟨k, mod_cast hk⟩

Result:
no goals

Proof state:
case intro.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : ↑n = 0
⊢ n ∣ m

case intro.inr.inl
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
h : k = 0
⊢ n ∣ m

case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Tactic:
iterate 2 simp only [h, mul_zero, zero_mul, Nat.cast_eq_zero] at hk; simp [hk]

Result:
case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Proof state:
case intro.inr.inl
n m : ℕ
k : Cardinal.{u_1}
h : k = 0
hk : m = 0
⊢ n ∣ m

case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Tactic:
simp [hk]

Result:
case intro.inr.inr.intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
hk' : k < ℵ₀
⊢ n ∣ m

Proof state:
case intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m

Tactic:
rw [hk, mul_lt_aleph0_iff] at this

Result:
case intro
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
-- Mathlib/Data/Finset/Image.lean
theorem mem_map_equiv {f : α ≃ β} {b : β} : b ∈ s.map f.toEmbedding ↔ f.symm b ∈ s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a ∈ s, f.toEmbedding a = b) → f.symm b ∈ s

Tactic:
rintro ⟨a, H, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
a : α
H : a ∈ s
⊢ f.symm (f.toEmbedding a) ∈ s

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
a : α
H : a ∈ s
⊢ f.symm (f.toEmbedding a) ∈ s

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a ∈ s, f.toEmbedding a = b) ↔ f.symm b ∈ s

Tactic:
exact
  ⟨by
    rintro ⟨a, H, rfl⟩
    simpa, fun h => ⟨_, h, by simp⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
h : f.symm b ∈ s
⊢ f.toEmbedding (f.symm b) = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ b ∈ map f.toEmbedding s ↔ f.symm b ∈ s

Tactic:
rw [mem_map]

Result:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ (∃ a ∈ s, f.toEmbedding a = b) ↔ f.symm b ∈ s
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem projKerOfRightInverse_apply_idem [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂)
    (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (x : LinearMap.ker f₁) :
    f₁.projKerOfRightInverse f₂ h x = x

Proof state:
R : Type u_1
inst✝⁹ : Ring R
R₂ : Type u_2
inst✝⁸ : Ring R₂
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
M₂ : Type u_5
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : IsTopologicalAddGroup M
f₁ : M →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M
h : Function.RightInverse ⇑f₂ ⇑f₁
x : ↥(LinearMap.ker f₁)
⊢ (f₁.projKerOfRightInverse f₂ h) ↑x = x

Tactic:
ext1

Result:
case a
R : Type u_1
inst✝⁹ : Ring R
R₂ : Type u_2
inst✝⁸ : Ring R₂
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
M₂ : Type u_5
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : IsTopologicalAddGroup M
f₁ : M →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M
h : Function.RightInverse ⇑f₂ ⇑f₁
x : ↥(LinearMap.ker f₁)
⊢ ↑((f₁.projKerOfRightInverse f₂ h) ↑x) = ↑x

Proof state:
case a
R : Type u_1
inst✝⁹ : Ring R
R₂ : Type u_2
inst✝⁸ : Ring R₂
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
M₂ : Type u_5
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : IsTopologicalAddGroup M
f₁ : M →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M
h : Function.RightInverse ⇑f₂ ⇑f₁
x : ↥(LinearMap.ker f₁)
⊢ ↑((f₁.projKerOfRightInverse f₂ h) ↑x) = ↑x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma floorRoot_zero_right (n : ℕ) : floorRoot n 0 = 0

Proof state:
n : ℕ
⊢ n.floorRoot 0 = 0

Tactic:
simp [floorRoot]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem carrier.add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg q)
    (hb : b ∈ carrier f_deg q) : a + b ∈ carrier f_deg q

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ (proj 𝒜 i) a ^ m ∈ 𝒜 (m • i)

Tactic:
mem_tac

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac

Result:
no goals

Proof state:
case pos.e_a.e_x
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
g : ℕ → A⁰_ f :=
  fun j =>
    (m + m).choose j •
      if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ j * (proj 𝒜 i) b ^ (m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) b ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
        else
          HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } *
            HomogeneousLocalization.mk
              { deg := m * i, num := ⟨(proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j), ⋯⟩, den := ⟨f ^ i, ⋯⟩,
                den_mem := ⋯ }
j : ℕ
hj : j ∈ range (m + m + 1)
h2 : ¬m + m < j
h1 : j ≤ m
⊢ ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m + m - j) =
    ↑(((decompose 𝒜) a) i) ^ j * ↑(((decompose 𝒜) b) i) ^ (m - j) * ↑(((decompose 𝒜) b) i) ^ m

Tactic:
rw [mul_assoc, ← pow_add, add_comm (m - j), Nat.add_sub_assoc h1]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem carrier.add_mem (q : Spec.T A⁰_ f) {a b : A} (ha : a ∈ carrier f_deg q)
    (hb : b ∈ carrier f_deg q) : a + b ∈ carrier f_deg q

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
l : A⁰_ f := HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
⊢ (proj 𝒜 i) a ^ (j - m) * (proj 𝒜 i) b ^ (m + m - j) ∈ 𝒜 ?m.378290

R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
l : A⁰_ f := HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
⊢ m * i = ?m.378290

Tactic:
apply GradedMonoid.toGradedMul.mul_mem (i := (j-m) • i) (j := (m + m - j) • i) <;> mem_tac_aux

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
l : A⁰_ f := HomogeneousLocalization.mk { deg := m * i, num := ⟨(proj 𝒜 i) a ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ }
⊢ m * i = (j - m) • i + (m + m - j) • i

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)