harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem le_length_eraseIdx (l : List α) (i : Nat) : length l - 1 ≤ length (l.eraseIdx i)

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.length - 1 ≤ (l.eraseIdx i).length

Tactic:
rw [length_eraseIdx]

Result:
α : Type u_1
l : List α
i : Nat
⊢ l.length - 1 ≤ if i < l.length then l.length - 1 else l.length

Proof state:
α : Type u_1
l : List α
i : Nat
⊢ l.length - 1 ≤ if i < l.length then l.length - 1 else l.length

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem rank_span_set {s : Set M} (hs : LinearIndepOn R id s) : Module.rank R ↑(span R s) = #s

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R s) = #↑s

Tactic:
rw [← @setOf_mem_eq _ s, ← Subtype.range_coe_subtype]

Result:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R (range Subtype.val)) = #↑(range Subtype.val)

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R (range Subtype.val)) = #↑(range Subtype.val)

Tactic:
exact rank_span hs

Result:
no goals
-- Mathlib/Order/Rel/GaloisConnection.lean
theorem leftDual_mem_rightFixedPoint (J : Set α) : R.leftDual J ∈ R.rightFixedPoints

Proof state:
case a
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))

Tactic:
exact R.gc_leftDual_rightDual.l_u_le (R.leftDual J)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ R.leftDual J ∈ R.rightFixedPoints

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J

case a
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ R.leftDual J ≤ R.leftDual (R.rightDual (R.leftDual J))

Proof state:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ J ≤ R.rightDual (R.leftDual J)

Tactic:
exact R.gc_leftDual_rightDual.le_u_l J

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ R.leftDual (R.rightDual (R.leftDual J)) ≤ R.leftDual J

Tactic:
apply R.gc_leftDual_rightDual.monotone_l

Result:
case a.a
α : Type u_1
β : Type u_2
R : Rel α β
J : Set α
⊢ J ≤ R.rightDual (R.leftDual J)
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_ne_one (f : Perm α) : #f.support ≠ 1

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f = 1
⊢ #f.support ≠ 1

Tactic:
exact ne_of_eq_of_ne (card_support_eq_zero.mpr h) zero_ne_one

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support ≠ 1

Tactic:
by_cases h : f = 1

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f = 1
⊢ #f.support ≠ 1

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ¬f = 1
⊢ #f.support ≠ 1

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ¬f = 1
⊢ #f.support ≠ 1

Tactic:
exact ne_of_gt (one_lt_card_support_of_ne_one h)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.map_sSup_of_bddAbove {f : Ordinal.{u} → Ordinal.{v}} (H : IsNormal f)
    {s : Set Ordinal.{u}} (hs : BddAbove s) (hn : s.Nonempty) : f (sSup s) = sSup (f '' s)

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
s : Set Ordinal.{u}
hs : BddAbove s
hn : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
have := hn.to_subtype

Result:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
s : Set Ordinal.{u}
hs : BddAbove s
hn : s.Nonempty
this : Nonempty ↑s
⊢ f (sSup s) = sSup (f '' s)

Proof state:
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
s : Set Ordinal.{u}
hs : BddAbove s
hn : s.Nonempty
this : Nonempty ↑s
⊢ f (sSup s) = sSup (f '' s)

Tactic:
rw [sSup_eq_iSup', sSup_image', H.map_iSup_of_bddAbove]

Result:
case hg
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
s : Set Ordinal.{u}
hs : BddAbove s
hn : s.Nonempty
this : Nonempty ↑s
⊢ BddAbove (range Subtype.val)

Proof state:
case hg
f : Ordinal.{u} → Ordinal.{v}
H : IsNormal f
s : Set Ordinal.{u}
hs : BddAbove s
hn : s.Nonempty
this : Nonempty ↑s
⊢ BddAbove (range Subtype.val)

Tactic:
rwa [Subtype.range_coe_subtype, setOf_mem_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Basic.lean
theorem map_comp {F U : Type*} [Field F] [AddCommGroup U] [Module F U] {σ : K →+* L} {τ : L →+* F}
    {γ : K →+* F} [RingHomCompTriple σ τ γ] (f : V →ₛₗ[σ] W) (hf : Function.Injective f)
    (g : W →ₛₗ[τ] U) (hg : Function.Injective g) :
    map (g.comp f) (hg.comp hf) = map g hg ∘ map f hf

Proof state:
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
g : W →ₛₗ[τ] U
hg : Function.Injective ⇑g
⊢ map (g.comp f) ⋯ = map g hg ∘ map f hf

Tactic:
ext ⟨v⟩

Result:
case h.mk
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
g : W →ₛₗ[τ] U
hg : Function.Injective ⇑g
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map (g.comp f) ⋯ (Quot.mk (⇑(projectivizationSetoid K V)) v) =
    (map g hg ∘ map f hf) (Quot.mk (⇑(projectivizationSetoid K V)) v)

Proof state:
case h.mk
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
g : W →ₛₗ[τ] U
hg : Function.Injective ⇑g
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map (g.comp f) ⋯ (Quot.mk (⇑(projectivizationSetoid K V)) v) =
    (map g hg ∘ map f hf) (Quot.mk (⇑(projectivizationSetoid K V)) v)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Bousfield.lean
lemma W_of_isIso {X Y : C} (f : X ⟶ Y) [IsIso f] : W P f := fun Z _ => by
  constructor
  · intro g₁ g₂ _
    simpa only [← cancel_epi f]
  · intro g
    exact ⟨inv f ≫ g, by simp⟩

Proof state:
case right
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
g : X ⟶ Z
⊢ ∃ a, (fun g => f ≫ g) a = g

Tactic:
exact ⟨inv f ≫ g, by simp⟩

Result:
no goals

Proof state:
case left
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
g₁ g₂ : Y ⟶ Z
a✝ : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ g₁ = g₂

Tactic:
simpa only [← cancel_epi f]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Bijective fun g => f ≫ g

Tactic:
constructor

Result:
case left
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Injective fun g => f ≫ g

case right
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun g => f ≫ g

Proof state:
case right
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Surjective fun g => f ≫ g

Tactic:
intro g

Result:
case right
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
g : X ⟶ Z
⊢ ∃ a, (fun g => f ≫ g) a = g

Proof state:
case left
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Injective fun g => f ≫ g

Tactic:
intro g₁ g₂ _

Result:
case left
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
g₁ g₂ : Y ⟶ Z
a✝ : (fun g => f ≫ g) g₁ = (fun g => f ≫ g) g₂
⊢ g₁ = g₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
g : X ⟶ Z
⊢ (fun g => f ≫ g) (inv f ≫ g) = g

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem hasColimit_of_equivalence_comp (e : K ≌ J) [HasColimit (e.functor ⋙ F)] : HasColimit F

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
this : HasColimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasColimit F

Tactic:
apply hasColimitOfIso (e.invFunIdAssoc F).symm

Result:
no goals

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
⊢ HasColimit F

Tactic:
haveI : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_equivalence_comp e.symm

Result:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
this : HasColimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasColimit F
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_inf_distrib_left (s : Finset ι) (f : ι → α) (a : α) :
    a ⊓ s.sup f = s.sup fun i => a ⊓ f i

Proof state:
case empty
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
⊢ a ⊓ ∅.sup f = ∅.sup fun i => a ⊓ f i

Tactic:
simp_rw [Finset.sup_empty, inf_bot_eq]

Result:
no goals

Proof state:
case cons
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
h : a ⊓ s✝.sup f = s✝.sup fun i => a ⊓ f i
⊢ a ⊓ (cons a✝ s✝ h✝).sup f = (cons a✝ s✝ h✝).sup fun i => a ⊓ f i

Tactic:
rw [sup_cons, sup_cons, inf_sup_left, h]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a ⊓ s.sup f = s.sup fun i => a ⊓ f i

Tactic:
induction s using Finset.cons_induction with
| empty => simp_rw [Finset.sup_empty, inf_bot_eq]
| cons _ _ _ h => rw [sup_cons, sup_cons, inf_sup_left, h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem neg [AddGroup β] [IsTopologicalAddGroup β] (hf : FinStronglyMeasurable f μ) :
    FinStronglyMeasurable (-f) μ

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support fun x => -(hf.approx n) x) < ⊤

Tactic:
rw [Function.support_neg (hf.approx n)]

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support ⇑(hf.approx n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
⊢ FinStronglyMeasurable (-f) μ

Tactic:
refine ⟨fun n => -hf.approx n, fun n => ?_, fun x => (hf.tendsto_approx x).neg⟩

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support ⇑((fun n => -hf.approx n) n)) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
this : μ (support fun x => -(hf.approx n) x) < ⊤
⊢ μ (support ⇑((fun n => -hf.approx n) n)) < ⊤

Tactic:
convert this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support ⇑((fun n => -hf.approx n) n)) < ⊤

Tactic:
suffices μ (Function.support fun x => -(hf.approx n) x) < ∞ by convert this

Result:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support fun x => -(hf.approx n) x) < ⊤

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddGroup β
inst✝ : IsTopologicalAddGroup β
hf : FinStronglyMeasurable f μ
n : ℕ
⊢ μ (support ⇑(hf.approx n)) < ⊤

Tactic:
exact hf.fin_support_approx n

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_zero (n : Num) : n + 0 = n

Proof state:
n : Num
⊢ n + 0 = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_biSup_u [CompleteLattice α] [CompleteLattice β] (gi : GaloisInsertion l u) {ι : Sort x}
    {p : ι → Prop} (f : ∀ i, p i → β) : l (⨆ (i) (hi), u (f i hi)) = ⨆ (i) (hi), f i hi

Proof state:
α : Type u
β : Type v
l : α → β
u : β → α
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
gi : GaloisInsertion l u
ι : Sort x
p : ι → Prop
f : (i : ι) → p i → β
⊢ l (⨆ i, ⨆ (hi : p i), u (f i hi)) = ⨆ i, ⨆ (hi : p i), f i hi

Tactic:
simp only [iSup_subtype', gi.l_iSup_u]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem toContinuousMap_comp_symm :
    (f : C(α, β)).comp (f.symm : C(β, α)) = ContinuousMap.id β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ (↑f).comp ↑f.symm = ContinuousMap.id β

Tactic:
rw [← coe_trans, symm_trans_self, coe_refl]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem support_cycleOf_le [DecidableEq α] [Fintype α] (f : Perm α) (x : α) :
    support (f.cycleOf x) ≤ support f

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (f.cycleOf x).support
⊢ y ∈ f.support

Tactic:
rw [mem_support, cycleOf_apply] at hy

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then f y else y) ≠ y
⊢ y ∈ f.support

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : f.SameCycle x y
hy : f y ≠ y
⊢ y ∈ f.support

Tactic:
exact mem_support.mpr hy

Result:
no goals

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Tactic:
exact absurd rfl hy

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : (if f.SameCycle x y then f y else y) ≠ y
⊢ y ∈ f.support

Tactic:
split_ifs at hy

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : f.SameCycle x y
hy : f y ≠ y
⊢ y ∈ f.support

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
h✝ : ¬f.SameCycle x y
hy : y ≠ y
⊢ y ∈ f.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ (f.cycleOf x).support ≤ f.support

Tactic:
intro y hy

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (f.cycleOf x).support
⊢ y ∈ f.support
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma Y_sub_Y_add_Y_sub_negY {P Q : Fin 3 → R} (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    (P y * Q z ^ 3 - Q y * P z ^ 3) + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) =
      (P y - W'.negY P) * Q z ^ 3

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) + -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - W'.negY P) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0

Tactic:
rw [negY, negY]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = (P y - W'.negY P) * Q z ^ 3

Tactic:
linear_combination (norm := (rw [negY, negY]; ring1)) -W'.a₁ * P z * Q z * hx

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0

Tactic:
ring1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negOfNat_mul_ofNat (m n : Nat) : negOfNat m * (n : Nat) = negOfNat (m * n)

Proof state:
m n : Nat
⊢ negOfNat m * ↑n = negOfNat (m * n)

Tactic:
rw [Int.mul_comm]

Result:
m n : Nat
⊢ ↑n * negOfNat m = negOfNat (m * n)

Proof state:
m n : Nat
⊢ ↑n * negOfNat m = negOfNat (m * n)

Tactic:
simp [ofNat_mul_negOfNat, Nat.mul_comm]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma Finset.univ_eq_elems {α : Type*} [Fintype α] (elems : Finset α)
    (complete : ∀ x : α, x ∈ elems) :
    Finset.univ = elems

Proof state:
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
⊢ Finset.univ = elems

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems

Proof state:
case h
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems

Tactic:
simpa using complete x

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem tails_eq_tailsTR : @tails = @tailsTR

Proof state:
α : Type u_1
l : List α
⊢ ∀ (acc : Array (List α)), tailsTR.go l acc = acc.toList ++ l.tails

Tactic:
induction l <;> simp [*, tailsTR.go]

Result:
no goals

Proof state:
case h
α : Type u_1
⊢ tails = tailsTR

Tactic:
have H (l : List α) : ∀ acc, tailsTR.go l acc = acc.toList ++ tails l := by
  induction l <;> simp [*, tailsTR.go]

Result:
case h
α : Type u_1
H : ∀ (l : List α) (acc : Array (List α)), tailsTR.go l acc = acc.toList ++ l.tails
⊢ tails = tailsTR

Proof state:
⊢ @tails = @tailsTR

Tactic:
funext α

Result:
case h
α : Type u_1
⊢ tails = tailsTR

Proof state:
case h
α : Type u_1
H : ∀ (l : List α) (acc : Array (List α)), tailsTR.go l acc = acc.toList ++ l.tails
⊢ tails = tailsTR

Tactic:
simp (config := { unfoldPartialApp := true }) [tailsTR, H]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_mod_opow_log_lt_log_self {b o : Ordinal} (hb : 1 < b) (hbo : b ≤ o) :
    log b (o % (b ^ log b o)) < log b o

Proof state:
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rcases eq_or_ne (o % (b ^ log b o)) 0 with h | h

Result:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o

case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o

Proof state:
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ 0 < b ^ log b o

Tactic:
exact opow_pos _ (zero_lt_one.trans hb)

Result:
no goals

Proof state:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o

Tactic:
exact log_pos hb (one_le_iff_ne_zero.1 (hb.le.trans hbo)) hbo

Result:
no goals

Proof state:
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ b ^ log b o ≠ 0

Tactic:
rw [← Ordinal.pos_iff_ne_zero]

Result:
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ 0 < b ^ log b o

Proof state:
case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rw [← succ_le_iff, succ_log_def hb h]

Result:
case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ sInf {o_1 | o % b ^ log b o < b ^ o_1} ≤ log b o

Proof state:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rw [h, log_zero_right]

Result:
case inl
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o = 0
⊢ 0 < log b o

Proof state:
case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ sInf {o_1 | o % b ^ log b o < b ^ o_1} ≤ log b o

Tactic:
apply csInf_le'

Result:
case inr.h
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b o ∈ {o_1 | o % b ^ log b o < b ^ o_1}

Proof state:
case inr.h
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b o ∈ {o_1 | o % b ^ log b o < b ^ o_1}

Tactic:
apply mod_lt

Result:
case inr.h.h
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ b ^ log b o ≠ 0
-- Mathlib/SetTheory/Cardinal/Finite.lean
theorem natCard_pos (hs : s.Finite) : 0 < Nat.card s ↔ s.Nonempty

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
⊢ 0 < Nat.card ↑s ↔ s.Nonempty

Tactic:
simp [pos_iff_ne_zero, Nat.card_eq_zero, hs.to_subtype, nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_mul {x y : ℂ} (z : ℂ) (h₁ : -π < (log x * y).im) (h₂ : (log x * y).im ≤ π) :
    x ^ (y * z) = (x ^ y) ^ z

Proof state:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)

Tactic:
split_ifs <;> simp_all [exp_ne_zero, log_exp h₁ h₂, mul_assoc]

Result:
no goals

Proof state:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ x ^ (y * z) = (x ^ y) ^ z

Tactic:
simp only [cpow_def]

Result:
x y z : ℂ
h₁ : -π < (log x * y).im
h₂ : (log x * y).im ≤ π
⊢ (if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) =
    if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0
    else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)