harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_range_card (g : Equiv.Perm α) :
    Fintype.card (kerParam g).range = (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g x : Perm α
hx : x ∈ g.cycleFactorsFinset
⊢ Fintype.card ↥(zpowers x) = (Finset.card ∘ support) x

Tactic:
rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card ↥(kerParam g).range = (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
rw [Fintype.card_coeSort_range (kerParam_injective g)]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card (Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c))) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Fintype.card (Perm ↑(Function.fixedPoints ⇑g) × ((c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c))) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
rw [Fintype.card_prod, Fintype.card_perm, Fintype.card_pi, card_fixedPoints]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card α - g.cycleType.sum)! * ∏ i : { x // x ∈ g.cycleFactorsFinset }, Fintype.card ↥(zpowers ↑i) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∏ i : { x // x ∈ g.cycleFactorsFinset }, Fintype.card ↥(zpowers ↑i) = g.cycleType.prod

Tactic:
rw [Finset.univ_eq_attach, g.cycleFactorsFinset.prod_attach (fun i ↦ Fintype.card (zpowers i)),
  cycleType, Finset.prod_map_val]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∏ x ∈ g.cycleFactorsFinset, Fintype.card ↥(zpowers x) = ∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∏ x ∈ g.cycleFactorsFinset, Fintype.card ↥(zpowers x) = ∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a

Tactic:
refine Finset.prod_congr rfl (fun x hx ↦ ?_)

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g x : Perm α
hx : x ∈ g.cycleFactorsFinset
⊢ Fintype.card ↥(zpowers x) = (Finset.card ∘ support) x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (Fintype.card α - g.cycleType.sum)! * ∏ i : { x // x ∈ g.cycleFactorsFinset }, Fintype.card ↥(zpowers ↑i) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
apply congr_arg

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ ∏ i : { x // x ∈ g.cycleFactorsFinset }, Fintype.card ↥(zpowers ↑i) = g.cycleType.prod
-- Mathlib/Analysis/RCLike/Basic.lean
theorem real_smul_eq_coe_smul [AddCommGroup E] [Module K E] [Module ℝ E] [IsScalarTower ℝ K E]
    (r : ℝ) (x : E) : r • x = (r : K) • x

Proof state:
K : Type u_1
E : Type u_2
inst✝⁴ : RCLike K
inst✝³ : AddCommGroup E
inst✝² : Module K E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ K E
r : ℝ
x : E
⊢ r • x = ↑r • x

Tactic:
rw [RCLike.ofReal_alg, smul_one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux as [] ++ bs

Proof state:
case cons
α : Type u
a : α
as : List α
ih : ∀ (bs : List α), as.reverseAux bs = as.reverseAux nil ++ bs
bs : List α
⊢ as.reverseAux nil ++ a :: bs = as.reverseAux nil ++ (a :: nil ++ bs)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u
a : α
as : List α
ih : ∀ (bs : List α), as.reverseAux bs = as.reverseAux nil ++ bs
bs : List α
⊢ as.reverseAux (a :: bs) = as.reverseAux (a :: nil) ++ bs

Tactic:
rw [ih (a :: bs), ih [a], append_assoc]

Result:
case cons
α : Type u
a : α
as : List α
ih : ∀ (bs : List α), as.reverseAux bs = as.reverseAux nil ++ bs
bs : List α
⊢ as.reverseAux nil ++ a :: bs = as.reverseAux nil ++ (a :: nil ++ bs)

Proof state:
case nil
α : Type u
bs : List α
⊢ nil.reverseAux bs = nil.reverseAux nil ++ bs

Tactic:
simp [reverseAux]

Result:
no goals

Proof state:
case cons
α : Type u
a : α
as : List α
ih : ∀ (bs : List α), as.reverseAux bs = as.reverseAux nil ++ bs
bs : List α
⊢ (a :: as).reverseAux bs = (a :: as).reverseAux nil ++ bs

Tactic:
simp [reverseAux]

Result:
case cons
α : Type u
a : α
as : List α
ih : ∀ (bs : List α), as.reverseAux bs = as.reverseAux nil ++ bs
bs : List α
⊢ as.reverseAux (a :: bs) = as.reverseAux (a :: nil) ++ bs

Proof state:
α : Type u
as bs : List α
⊢ as.reverseAux bs = as.reverseAux nil ++ bs

Tactic:
induction as generalizing bs with
| nil => simp [reverseAux]
| cons a as ih =>
  simp [reverseAux]
  rw [ih (a :: bs), ih [a], append_assoc]
  rfl

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem mk_eq_of_naturality {f g f' : C} {η θ : f ⟶ g} {η' θ' : f ≅ g}
    (η_f : 𝟙_ C ⊗ f ≅ f') (η_g : 𝟙_ C ⊗ g ≅ f')
    (η_hom : η'.hom = η) (Θ_hom : θ'.hom = θ)
    (Hη : whiskerLeftIso (𝟙_ C) η' ≪≫ η_g = η_f)
    (Hθ : whiskerLeftIso (𝟙_ C) θ' ≪≫ η_g = η_f) : η = θ :=
  calc
    η = η'.hom := η_hom.symm
    _ = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ η'.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hη)]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g f' : C
η θ : f ⟶ g
η' θ' : f ≅ g
η_f : 𝟙_ C ⊗ f ≅ f'
η_g : 𝟙_ C ⊗ g ≅ f'
η_hom : η'.hom = η
Θ_hom : θ'.hom = θ
Hη : 𝟙_ C ◁ η' ≪≫ η_g = η_f
Hθ : 𝟙_ C ◁ θ' ≪≫ η_g = η_f
⊢ (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom = θ'.hom

Tactic:
simp [← reassoc_of% (congrArg Iso.hom Hθ)]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem neighborSet_sInf (s : Set G.Subgraph) (v : V) :
    (sInf s).neighborSet v = (⋂ G' ∈ s, neighborSet G' v) ∩ G.neighborSet v

Proof state:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
⊢ (sInf s).neighborSet v = (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v

Tactic:
ext

Result:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x✝ : V
⊢ x✝ ∈ (sInf s).neighborSet v ↔ x✝ ∈ (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v

Proof state:
case h
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x✝ : V
⊢ x✝ ∈ (sInf s).neighborSet v ↔ x✝ ∈ (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/ClassEquation.lean
theorem Group.nat_card_center_add_sum_card_noncenter_eq_card [Finite G] :
    Nat.card (Subgroup.center G) + ∑ᶠ x ∈ noncenter G, Nat.card x.carrier = Nat.card G

Proof state:
case intro.e_a.convert_7
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ {x : ConjClasses G}, Fintype.card ↑x.carrier ≠ 0 → (x ∈ noncenter G ↔ x ∈ (noncenter G).toFinset)

Tactic:
simp [Set.mem_toFinset]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↑(noncenter G)ᶜ = (Finset.univ \ (noncenter G).toFinset).card

Tactic:
rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Group.lean
theorem tendsto_atTop_add_left_of_le' (C : β) (hf : ∀ᶠ x in l, C ≤ f x) (hg : Tendsto g l atTop) :
    Tendsto (fun x => f x + g x) l atTop :=
  .atTop_of_isBoundedUnder_le_add (f := -f) ⟨-C, by simpa⟩ (by simpa)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ ∀ᶠ (x : β) in map (-f) l, (fun x1 x2 => x1 ≤ x2) x (-C)

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : OrderedAddCommGroup β
l : Filter α
f g : α → β
C : β
hf : ∀ᶠ (x : α) in l, C ≤ f x
hg : Tendsto g l atTop
⊢ Tendsto (fun x => (-f) x + (f x + g x)) l atTop

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem antilipschitz (hf : ApproximatesLinearOn f (f' : E →L[𝕜] F) s c)
    (hc : Subsingleton E ∨ c < N⁻¹) : AntilipschitzWith (N⁻¹ - c)⁻¹ (s.restrict f)

Proof state:
case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)

Tactic:
convert (f'.antilipschitz.restrict s).add_lipschitzWith hf.lipschitz_sub hc

Result:
case h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : c < ‖↑f'.symm‖₊⁻¹
x✝ : ↑s
⊢ s.restrict f x✝ = s.restrict (⇑f') x✝ + (f ↑x✝ - ↑f' ↑x✝)

Proof state:
case h.e'_6.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : c < ‖↑f'.symm‖₊⁻¹
x✝ : ↑s
⊢ s.restrict f x✝ = s.restrict (⇑f') x✝ + (f ↑x✝ - ↑f' ↑x✝)

Tactic:
simp [restrict]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹
⊢ AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)

Tactic:
rcases hc with hE | hc

Result:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hE : Subsingleton E
⊢ AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)

case inr
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : c < ‖↑f'.symm‖₊⁻¹
⊢ AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)

Proof state:
case inl
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
s : Set E
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hE : Subsingleton E
⊢ AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.restrict f)

Tactic:
exact AntilipschitzWith.of_subsingleton

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem secondCountable_of_almost_dense_set
    (H : ∀ ε > (0 : ℝ), ∃ s : Set α, s.Countable ∧ ∀ x, ∃ y ∈ s, dist x y ≤ ε) :
    SecondCountableTopology α

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 ε0 with ⟨ε', ε'0, ε'ε⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
refine EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_

Result:
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
x : α
⊢ edist x (y x) ≤ ↑ε'

Tactic:
exact mod_cast hyx x

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ

Tactic:
choose s hsc y hys hyx using H ε' (mod_cast ε'0)

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, EMetric.closedBall x ε = univ

Tactic:
refine ⟨s, hsc, iUnion₂_eq_univ_iff.2 fun x => ⟨y x, hys _, le_trans ?_ ε'ε.le⟩⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
ε' : ℝ≥0
ε'0 : 0 < ↑ε'
ε'ε : ↑ε' < ε
s : Set α
hsc : s.Countable
y : α → α
hys : ∀ (x : α), y x ∈ s
hyx : ∀ (x : α), dist x (y x) ≤ ↑ε'
x : α
⊢ edist x (y x) ≤ ↑ε'
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_iff_mod : l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l'

Proof state:
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).length > 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n ≤ l.length, l.rotate n = l'

Tactic:
obtain ⟨n, rfl⟩ := h

Result:
case intro
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1 ≤ l.length, l.rotate n_1 = l.rotate n

Proof state:
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % (hd :: tl).length ≤ (hd :: tl).length

Tactic:
refine (Nat.mod_lt _ ?_).le

Result:
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ (hd :: tl).length > 0

Proof state:
case intro
α : Type u
l : List α
n : ℕ
⊢ ∃ n_1 ≤ l.length, l.rotate n_1 = l.rotate n

Tactic:
rcases l with - | ⟨hd, tl⟩

Result:
case intro.nil
α : Type u
n : ℕ
⊢ ∃ n_1 ≤ [].length, [].rotate n_1 = [].rotate n

case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1 ≤ (hd :: tl).length, (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Proof state:
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ ∃ n_1 ≤ (hd :: tl).length, (hd :: tl).rotate n_1 = (hd :: tl).rotate n

Tactic:
refine ⟨n % (hd :: tl).length, ?_, rotate_mod _ _⟩

Result:
case intro.cons
α : Type u
n : ℕ
hd : α
tl : List α
⊢ n % (hd :: tl).length ≤ (hd :: tl).length

Proof state:
case intro.nil
α : Type u
n : ℕ
⊢ ∃ n_1 ≤ [].length, [].rotate n_1 = [].rotate n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l l' : List α
⊢ l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l'

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

Result:
α : Type u
l l' : List α
h : l ~r l'
⊢ ∃ n ≤ l.length, l.rotate n = l'
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
lemma natLog_le_logb (a b : ℕ) : Nat.log b a ≤ Real.logb b a

Proof state:
a b : ℕ
⊢ ↑(Nat.log b a) ≤ ↑⌊logb ↑b ↑a⌋

Tactic:
rw [Real.floor_logb_natCast (Nat.cast_nonneg a), Int.log_natCast, Int.cast_natCast]

Result:
no goals

Proof state:
a b : ℕ
⊢ ↑(Nat.log b a) ≤ logb ↑b ↑a

Tactic:
apply le_trans _ (Int.floor_le ((b : ℝ).logb a))

Result:
a b : ℕ
⊢ ↑(Nat.log b a) ≤ ↑⌊logb ↑b ↑a⌋
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma Q_map_comp_Qinv {X Y Y' : C} (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s) :
    (Q W).map f ≫ Qinv s hs = homMk (mk f s hs)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (ofInv s hs).f ≫ (ofHom W (𝟙 (ofHom W f).Y')).s = (ofHom W f).s ≫ (ofHom W (𝟙 (ofHom W f).Y')).f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk ((ofHom W f).comp₀ (ofInv s hs) (ofHom W (𝟙 (ofHom W f).Y'))) = homMk (mk f s hs)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk (ofHom W f) ≫ homMk (ofInv s hs) = homMk (mk f s hs)

Tactic:
rw [homMk_comp_homMk (ofHom W f) (ofInv s hs) (ofHom W (𝟙 _)) (by simp)]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk ((ofHom W f).comp₀ (ofInv s hs) (ofHom W (𝟙 (ofHom W f).Y'))) = homMk (mk f s hs)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (Q W).map f ≫ Qinv s hs = homMk (mk f s hs)

Tactic:
dsimp only [Q_map, Qinv]

Result:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk (ofHom W f) ≫ homMk (ofInv s hs) = homMk (mk f s hs)
-- Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean
@[simp, nolint unusedHavesSuffices] -- false positive from unfolding galRestrictHom
lemma galRestrictHom_symm_algebraMap_apply (σ : B →ₐ[A] B) (x : B) :
    (galRestrictHom A K L B).symm σ (algebraMap B L x) = algebraMap B L (σ x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B
x : B
this : IsDomain A
⊢ ((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)

Tactic:
have := IsIntegralClosure.isLocalization A K L B

Result:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B
x : B
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
⊢ ((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B
x : B
⊢ ((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)

Tactic:
have := (IsFractionRing.injective A K).isDomain

Result:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B
x : B
this : IsDomain A
⊢ ((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)

Proof state:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B
x : B
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
⊢ ((galRestrictHom A K L B).symm σ) ((algebraMap B L) x) = (algebraMap B L) (σ x)

Tactic:
simp [galRestrictHom, galLift, Subalgebra.algebraMap_eq]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Finite.iUnion {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Finite)
    (hs : ∀ i ∈ t, (s i).Finite) (he : ∀ i, i ∉ t → s i = ∅) : (⋃ i, s i).Finite

Proof state:
case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : False
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ ⋃ i, s i ⊆ ⋃ i ∈ t, s i

Tactic:
refine iUnion_subset fun i x hx => ?_

Result:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ x ∈ ⋃ i ∈ t, s i

Proof state:
case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
rw [he i hi, mem_empty_iff_false] at hx

Result:
case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : False
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ (⋃ i, s i).Finite

Tactic:
suffices ⋃ i, s i ⊆ ⋃ i ∈ t, s i by exact (ht.biUnion hs).subset this

Result:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
⊢ ⋃ i, s i ⊆ ⋃ i ∈ t, s i

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
by_cases hi : i ∈ t

Result:
case pos
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ x ∈ ⋃ i ∈ t, s i

case neg
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∉ t
⊢ x ∈ ⋃ i ∈ t, s i

Proof state:
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
this : ⋃ i, s i ⊆ ⋃ i ∈ t, s i
⊢ (⋃ i, s i).Finite

Tactic:
exact (ht.biUnion hs).subset this

Result:
no goals

Proof state:
case pos
α : Type u
ι : Type u_1
s : ι → Set α
t : Set ι
ht : t.Finite
hs : ∀ i ∈ t, (s i).Finite
he : ∀ i ∉ t, s i = ∅
i : ι
x : α
hx : x ∈ s i
hi : i ∈ t
⊢ x ∈ ⋃ i ∈ t, s i

Tactic:
exact mem_biUnion hi hx

Result:
no goals