harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem Disjoint.cycleType_mul {f g : Perm α} (h : f.Disjoint g) :
    (f * g).cycleType = f.cycleType + g.cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).cycleType = f.cycleType + g.cycleType

Tactic:
simp only [Perm.cycleType]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ Multiset.map (Finset.card ∘ support) (f * g).cycleFactorsFinset.val =
    Multiset.map (Finset.card ∘ support) f.cycleFactorsFinset.val +
      Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset.val g.cycleFactorsFinset.val

Tactic:
simp only [Finset.disjoint_val, Disjoint.disjoint_cycleFactorsFinset h]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ Multiset.map (fun x => x.support.card) (f.cycleFactorsFinset.val ∪ g.cycleFactorsFinset.val) =
    Multiset.map (fun x => x.support.card) f.cycleFactorsFinset.val +
      Multiset.map (fun x => x.support.card) g.cycleFactorsFinset.val

Tactic:
rw [← Multiset.add_eq_union_iff_disjoint.mpr _, Multiset.map_add]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.cycleFactorsFinset.val g.cycleFactorsFinset.val

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ Multiset.map (Finset.card ∘ support) (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).val =
    Multiset.map (Finset.card ∘ support) f.cycleFactorsFinset.val +
      Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
simp only [Finset.union_val, Function.comp_apply]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ Multiset.map (fun x => x.support.card) (f.cycleFactorsFinset.val ∪ g.cycleFactorsFinset.val) =
    Multiset.map (fun x => x.support.card) f.cycleFactorsFinset.val +
      Multiset.map (fun x => x.support.card) g.cycleFactorsFinset.val

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ Multiset.map (Finset.card ∘ support) (f * g).cycleFactorsFinset.val =
    Multiset.map (Finset.card ∘ support) f.cycleFactorsFinset.val +
      Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val

Tactic:
rw [h.cycleFactorsFinset_mul_eq_union]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f g : Perm α
h : f.Disjoint g
⊢ Multiset.map (Finset.card ∘ support) (f.cycleFactorsFinset ∪ g.cycleFactorsFinset).val =
    Multiset.map (Finset.card ∘ support) f.cycleFactorsFinset.val +
      Multiset.map (Finset.card ∘ support) g.cycleFactorsFinset.val
-- Mathlib/CategoryTheory/Localization/Construction.lean
theorem natTransExtension_hcomp {F G : W.Localization ⥤ D} (τ : W.Q ⋙ F ⟶ W.Q ⋙ G) :
    𝟙 W.Q ◫ natTransExtension τ = τ

Proof state:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ : W.Q ⋙ F ⟶ W.Q ⋙ G
⊢ 𝟙 W.Q ◫ natTransExtension τ = τ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
/--
The Krull dimension is the supremum of the elements' coheights.

This version of the lemma assumes that `α` is nonempty. In this case, the coercion from `ℕ∞` to
`WithBot ℕ∞` is on the outside of the right-hand side, which is usually more convenient.

If `α` were empty, then `krullDim α = ⊥`. See `krullDim_eq_iSup_coheight` for the more general
version, with the coercion under the supremum.
-/
lemma krullDim_eq_iSup_coheight_of_nonempty [Nonempty α] :
    krullDim α = ↑(⨆ (a : α), coheight a)

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim α = ↑(⨆ a, coheight a)

Tactic:
simpa using krullDim_eq_iSup_height_of_nonempty (α := αᵒᵈ)

Result:
no goals
-- Mathlib/Analysis/ODE/PicardLindelof.lean
theorem dist_iterate_next_apply_le (f₁ f₂ : FunSpace v) (n : ℕ) (t : Icc v.tMin v.tMax) :
    dist (next^[n] f₁ t) (next^[n] f₂ t) ≤ (v.L * |t.1 - v.t₀|) ^ n / n ! * dist f₁ f₂

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist ((next^[n] f₁).toFun t) ((next^[n] f₂).toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[n] f₁).next.toFun t) ((next^[n] f₂).next.toFun t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * dist f₁ f₂

Tactic:
exact dist_next_apply_le_of_le ihn _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[n] f₁).toFun t) ((next^[n] f₂).toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂

Tactic:
induction n generalizing t with
| zero =>
  rw [pow_zero, Nat.factorial_zero, Nat.cast_one, div_one, one_mul]
  exact dist_apply_le_dist f₁ f₂ t
| succ n ihn =>
  rw [iterate_succ_apply', iterate_succ_apply']
  exact dist_next_apply_le_of_le ihn _

Result:
no goals

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[0] f₁).toFun t) ((next^[0] f₂).toFun t) ≤ dist f₁ f₂

Tactic:
exact dist_apply_le_dist f₁ f₂ t

Result:
no goals

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist ((next^[n] f₁).toFun t) ((next^[n] f₂).toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[n + 1] f₁).toFun t) ((next^[n + 1] f₂).toFun t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * dist f₁ f₂

Tactic:
rw [iterate_succ_apply', iterate_succ_apply']

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
n : ℕ
ihn :
  ∀ (t : ↑(Icc v.tMin v.tMax)),
    dist ((next^[n] f₁).toFun t) ((next^[n] f₂).toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ n / ↑n ! * dist f₁ f₂
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[n] f₁).next.toFun t) ((next^[n] f₂).next.toFun t) ≤
    (↑v.L * |↑t - ↑v.t₀|) ^ (n + 1) / ↑(n + 1)! * dist f₁ f₂

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[0] f₁).toFun t) ((next^[0] f₂).toFun t) ≤ (↑v.L * |↑t - ↑v.t₀|) ^ 0 / ↑0! * dist f₁ f₂

Tactic:
rw [pow_zero, Nat.factorial_zero, Nat.cast_one, div_one, one_mul]

Result:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
v : PicardLindelof E
f₁ f₂ : v.FunSpace
t : ↑(Icc v.tMin v.tMax)
⊢ dist ((next^[0] f₁).toFun t) ((next^[0] f₂).toFun t) ≤ dist f₁ f₂
-- Mathlib/Analysis/RCLike/Lemmas.lean
lemma RCLike.span_one_I : Submodule.span ℝ (M := K) {1, I} = ⊤

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ ∀ (x : K), ∃ a b, a • 1 + b • I = x

Tactic:
exact fun x ↦ ⟨re x, im x, by simp [real_smul_eq_coe_mul]⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re x • 1 + im x • I = x

Tactic:
simp [real_smul_eq_coe_mul]

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ Submodule.span ℝ {1, I} = ⊤

Tactic:
suffices ∀ x : K, ∃ a b : ℝ, a • 1 + b • I = x by
  simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]

Result:
K : Type u_1
inst✝ : RCLike K
⊢ ∀ (x : K), ∃ a b, a • 1 + b • I = x

Proof state:
K : Type u_1
inst✝ : RCLike K
this : ∀ (x : K), ∃ a b, a • 1 + b • I = x
⊢ Submodule.span ℝ {1, I} = ⊤

Tactic:
simpa [Submodule.eq_top_iff', Submodule.mem_span_pair]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
lemma Nat.max_log_padicValNat_succ_eq_log_succ (n : ℕ) :
    max (log 2 n) (padicValNat 2 (n + 1)) = log 2 (n + 1)

Proof state:
n : ℕ
⊢ log 2 (n + 1) ≤ log 2 n ⊔ padicValNat 2 (n + 1)

Tactic:
rw [le_max_iff, or_iff_not_imp_left, not_le]

Result:
n : ℕ
⊢ log 2 n < log 2 (n + 1) → log 2 (n + 1) ≤ padicValNat 2 (n + 1)

Proof state:
n : ℕ
h : n + 1 = 2 ^ log 2 (n + 1)
⊢ log 2 (n + 1) ≤ padicValNat 2 (n + 1)

Tactic:
rw [h, padicValNat.prime_pow, ← h]

Result:
no goals

Proof state:
n : ℕ
⊢ log 2 n ⊔ padicValNat 2 (n + 1) = log 2 (n + 1)

Tactic:
apply le_antisymm (max_le (le_log_of_pow_le one_lt_two (pow_log_le_add_one 2 n))
  (padicValNat_le_nat_log (n + 1)))

Result:
n : ℕ
⊢ log 2 (n + 1) ≤ log 2 n ⊔ padicValNat 2 (n + 1)

Proof state:
n : ℕ
⊢ log 2 n < log 2 (n + 1) → log 2 (n + 1) ≤ padicValNat 2 (n + 1)

Tactic:
intro h

Result:
n : ℕ
h : log 2 n < log 2 (n + 1)
⊢ log 2 (n + 1) ≤ padicValNat 2 (n + 1)

Proof state:
n : ℕ
h : log 2 n < log 2 (n + 1)
⊢ log 2 (n + 1) ≤ padicValNat 2 (n + 1)

Tactic:
replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt one_lt_two h))
  (pow_log_le_self 2 n.succ_ne_zero)

Result:
n : ℕ
h : n + 1 = 2 ^ log 2 (n + 1)
⊢ log 2 (n + 1) ≤ padicValNat 2 (n + 1)
-- Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean
theorem map_projective (adj : F ⊣ G) [G.PreservesEpimorphisms] (P : C) (hP : Projective P) :
    Projective (F.obj P) where
  factors f g _

Proof state:
case intro
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ f', f' ≫ g = f

Tactic:
use F.map f' ≫ adj.counit.app _

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f

Tactic:
rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f

Tactic:
rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩

Result:
case intro
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ f', f' ≫ g = f
-- Mathlib/Topology/Connected/Basic.lean
theorem connectedSpace_iff_connectedComponent :
    ConnectedSpace α ↔ ∃ x : α, connectedComponent x = univ

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∃ x, connectedComponent x = univ) → ConnectedSpace α

Tactic:
rintro ⟨x, h⟩

Result:
case mpr.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ ConnectedSpace α

Proof state:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α → ∃ x, connectedComponent x = univ

Tactic:
rintro ⟨⟨x⟩⟩

Result:
case mp.mk.intro
α : Type u
inst✝ : TopologicalSpace α
toPreconnectedSpace✝ : PreconnectedSpace α
x : α
⊢ ∃ x, connectedComponent x = univ

Proof state:
case mpr.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ ConnectedSpace α

Tactic:
haveI : PreconnectedSpace α :=
  ⟨by rw [← h]; exact isPreconnected_connectedComponent⟩

Result:
case mpr.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α

Proof state:
case mp.mk.intro
α : Type u
inst✝ : TopologicalSpace α
toPreconnectedSpace✝ : PreconnectedSpace α
x : α
⊢ ∃ x, connectedComponent x = univ

Tactic:
exact
  ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩

Result:
no goals

Proof state:
case mpr.intro
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
this : PreconnectedSpace α
⊢ ConnectedSpace α

Tactic:
exact ⟨⟨x⟩⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α ↔ ∃ x, connectedComponent x = univ

Tactic:
constructor

Result:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α → ∃ x, connectedComponent x = univ

case mpr
α : Type u
inst✝ : TopologicalSpace α
⊢ (∃ x, connectedComponent x = univ) → ConnectedSpace α

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)

Tactic:
exact isPreconnected_connectedComponent

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected univ

Tactic:
rw [← h]

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)
-- Mathlib/GroupTheory/Transfer.lean
theorem isComplement' (hP : IsCyclic P) :
    (MonoidHom.transferSylow P (hP.normalizer_le_centralizer hp)).ker.IsComplement' P

Proof state:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
have := (Nat.card_eq_one_iff_unique.mp hn).1

Result:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Proof state:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
by_cases hn : Nat.card G = 1

Result:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Proof state:
case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
exact MonoidHom.ker_transferSylow_isComplement' P (hP.normalizer_le_centralizer rfl)

Result:
no goals

Proof state:
case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
have := Fact.mk (Nat.minFac_prime hn)

Result:
case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Proof state:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : (Nat.card G).minFac = p
P : Sylow p G
hP : IsCyclic ↥↑P
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
subst hp

Result:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Proof state:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ (MonoidHom.transferSylow P ⋯).ker.IsComplement' ↑P

Tactic:
rw [Subsingleton.elim (MonoidHom.transferSylow P (hP.normalizer_le_centralizer rfl)).ker ⊥,
  Subsingleton.elim P.1 ⊤]

Result:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ⊤

Proof state:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ ⊥.IsComplement' ⊤

Tactic:
exact isComplement'_bot_top

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma Spec_map_tensorInl_fromSpecResidueField :
    (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f =
      (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s

Tactic:
simp only [← Category.assoc, ← Spec.map_comp, pushout.condition]

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f = (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g

Tactic:
simp only [residueFieldCongr_inv, Category.assoc, tensorInl, tensorInr,
  ← Hom.Spec_map_residueFieldMap_fromSpecResidueField]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ S.fromSpecResidueField ((ConcreteCategory.hom f.base) T.x) =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ S.fromSpecResidueField ((ConcreteCategory.hom g.base) T.y)

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ S.fromSpecResidueField ((ConcreteCategory.hom f.base) T.x) =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ S.fromSpecResidueField ((ConcreteCategory.hom g.base) T.y)

Tactic:
rw [← residueFieldCongr_fromSpecResidueField T.hx.symm,
  ← residueFieldCongr_fromSpecResidueField T.hy.symm]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ Spec.map
        (pushout.inl ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap f T.x) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s =
    Spec.map
        (pushout.inr ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap f T.x)
          ((residueFieldCongr ⋯).hom ≫ Hom.residueFieldMap g T.y)) ≫
      Spec.map (Hom.residueFieldMap g T.y) ≫ Spec.map (residueFieldCongr ⋯).hom ≫ S.fromSpecResidueField T.s
-- Mathlib/SetTheory/Game/Basic.lean
theorem add_lf_add_left : ∀ {b c : Game} (_ : b ⧏ c) (a), (a + b : Game) ⧏ a + c

Proof state:
⊢ ∀ {b c : Game}, b ⧏ c → ∀ (a : Game), a + b ⧏ a + c

Tactic:
rintro ⟨b⟩ ⟨c⟩ h ⟨a⟩

Result:
case mk.mk.mk
b✝ : Game
b : PGame
c✝ : Game
c : PGame
h : Quot.mk (⇑setoid) b ⧏ Quot.mk (⇑setoid) c
a✝ : Game
a : PGame
⊢ Quot.mk (⇑setoid) a + Quot.mk (⇑setoid) b ⧏ Quot.mk (⇑setoid) a + Quot.mk (⇑setoid) c

Proof state:
case mk.mk.mk
b✝ : Game
b : PGame
c✝ : Game
c : PGame
h : Quot.mk (⇑setoid) b ⧏ Quot.mk (⇑setoid) c
a✝ : Game
a : PGame
⊢ Quot.mk (⇑setoid) a + Quot.mk (⇑setoid) b ⧏ Quot.mk (⇑setoid) a + Quot.mk (⇑setoid) c

Tactic:
apply PGame.add_lf_add_left h

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_mul_add [Semiring α] (x : α) (n : ℕ) :
    (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
have := (Commute.one_right x).geom_sum₂_mul_add n

Result:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Proof state:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
exact this

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i * 1 ^ (n - 1 - i)) * x + 1 ^ n = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n

Tactic:
rw [one_pow, geom_sum₂_with_one] at this

Result:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
this : (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
⊢ (∑ i ∈ range n, (x + 1) ^ i) * x + 1 = (x + 1) ^ n
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_le_floor_add_one (a : α) : ⌈a⌉ ≤ ⌊a⌋ + 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ a ≤ ↑⌊a⌋ + 1

Tactic:
exact (lt_floor_add_one a).le

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌈a⌉ ≤ ⌊a⌋ + 1

Tactic:
rw [ceil_le, Int.cast_add, Int.cast_one]

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ a ≤ ↑⌊a⌋ + 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_mapFinIdx {l : Vector α n}
    {f : (i : Nat) → α → (h : i < n) → β}
    {g : (i : Nat) → β → (h : i < n) → γ} :
    (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx (fun i a h => g i (f i a h) h)

Proof state:
α : Type u_1
n : Nat
β : Type u_2
γ : Type u_3
l : Vector α n
f : (i : Nat) → α → i < n → β
g : (i : Nat) → β → i < n → γ
⊢ (l.mapFinIdx f).mapFinIdx g = l.mapFinIdx fun i a h => g i (f i a h) h

Tactic:
simp [mapFinIdx_eq_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma surjective_of_isDominant_of_isClosed_range (f : X ⟶ Y) [IsDominant f]
    (hf : IsClosed (Set.range f.base)) :
    Surjective f :=
  ⟨by rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]⟩

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsDominant f
hf : IsClosed (Set.range ⇑(ConcreteCategory.hom f.base))
⊢ Function.Surjective ⇑(ConcreteCategory.hom f.base)

Tactic:
rw [← Set.range_eq_univ, ← hf.closure_eq, f.denseRange.closure_range]

Result:
no goals