harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/PGroup.lean
theorem exists_fixed_point_of_prime_dvd_card_of_fixed_point (hpα : p ∣ Nat.card α) {a : α}
    (ha : a ∈ fixedPoints G α) : ∃ b, b ∈ fixedPoints G α ∧ a ≠ b

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : 1 < Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
rw [Finite.one_lt_card_iff_nontrivial] at hα

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : ⟨b, hb⟩ ≠ ⟨a, ha⟩
hab : a = b
⊢ ⟨b, hb⟩ = ⟨a, ha⟩

Tactic:
simp_rw [hab]

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
have hα : 1 < Nat.card (fixedPoints G α) :=
  (Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (Finite.card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : 1 < Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
have hpf : p ∣ Nat.card (fixedPoints G α) :=
  Nat.modEq_zero_iff_dvd.mp ((hG.card_modEq_card_fixedPoints α).symm.trans hpα.modEq_zero_nat)

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
hpα : p ∣ Nat.card α
a : α
ha : a ∈ fixedPoints G α
hpf : p ∣ Nat.card ↑(fixedPoints G α)
hα : Nontrivial ↑(fixedPoints G α)
⊢ ∃ b ∈ fixedPoints G α, a ≠ b

Tactic:
exact
  let ⟨⟨b, hb⟩, hba⟩ := exists_ne (⟨a, ha⟩ : fixedPoints G α)
  ⟨b, hb, fun hab => hba (by simp_rw [hab])⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_prod_right_eq_zip {l : Array α} (f : α → β) :
    (l.map fun x => (f x, x)) = (l.map f).zip l

Proof state:
case e_bs
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun x => x) l = l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ (map f l).zip (map (fun x => x) l) = (map f l).zip l

Tactic:
congr

Result:
case e_bs
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun x => x) l = l

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun x => (f x, x)) l = (map f l).zip l

Tactic:
rw [← zip_map']

Result:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ (map f l).zip (map (fun x => x) l) = (map f l).zip l
-- Mathlib/Data/Finset/NAry.lean
theorem Finite.toFinset_image2 (f : α → β → γ) (hs : s.Finite) (ht : t.Finite)
    (hf := hs.image2 f ht) : hf.toFinset = Finset.image₂ f hs.toFinset ht.toFinset :=
  Finset.coe_injective <| by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
hf : optParam (image2 f s t).Finite ⋯
⊢ ↑(Finite.toFinset hf) = ↑(image₂ f hs.toFinset ht.toFinset)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_span_eq_card [Nontrivial R] {ι : Type*} [Fintype ι] {b : ι → M}
    (hb : LinearIndependent R b) :
    finrank R (span R (Set.range b)) = Fintype.card ι :=
  finrank_eq_of_rank_eq
    (by
      have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
      rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this)

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
  lift_eq_nat_iff] at this

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
@[simp]
lemma isNilpotent_toMatrix_iff (b : Basis ι R M) (f : M →ₗ[R] M) :
    IsNilpotent (toMatrix b b f) ↔ IsNilpotent f

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) f ^ k = 0 ↔ f ^ k = 0

Tactic:
rw [toMatrix_pow]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) (f ^ k) = 0 ↔ f ^ k = 0

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
⊢ IsNilpotent ((toMatrix b b) f) ↔ IsNilpotent f

Tactic:
refine exists_congr fun k ↦ ?_

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) f ^ k = 0 ↔ f ^ k = 0

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
ι : Type u_3
M : Type u_4
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
f : M →ₗ[R] M
k : ℕ
⊢ (toMatrix b b) (f ^ k) = 0 ↔ f ^ k = 0

Tactic:
exact (toMatrix b b).map_eq_zero_iff

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.iUnion [Countable ι] ⦃f : ι → Set α⦄
    (h : ∀ b, MeasurableSet (f b)) : MeasurableSet (⋃ b, f b)

Proof state:
case inl
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ b, f b)

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ b, f b)

Tactic:
rcases exists_surjective_nat ι with ⟨e, he⟩

Result:
case inr.intro
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ b, f b)

Proof state:
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
⊢ MeasurableSet (⋃ b, f b)

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : IsEmpty ι
⊢ MeasurableSet (⋃ b, f b)

case inr
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
⊢ MeasurableSet (⋃ b, f b)

Proof state:
case inr.intro
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ x, f (e x))

Tactic:
exact m.measurableSet_iUnion _ fun _ => h _

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ b, f b)

Tactic:
rw [← iUnion_congr_of_surjective _ he (fun _ => rfl)]

Result:
case inr.intro
α : Type u_1
ι : Sort u_6
m : MeasurableSpace α
inst✝ : Countable ι
f : ι → Set α
h : ∀ (b : ι), MeasurableSet (f b)
h✝ : Nonempty ι
e : ℕ → ι
he : Surjective e
⊢ MeasurableSet (⋃ x, f (e x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_map (f : β → α) (l : List β) : filter p (map f l) = map f (filter (p ∘ f) l)

Proof state:
case nil
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
⊢ filter p (map f []) = map f (filter (p ∘ f) [])

Tactic:
rfl

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
l : List β
⊢ filter p (map f l) = map f (filter (p ∘ f) l)

Tactic:
induction l with
| nil => rfl
| cons a l IH => by_cases h : p (f a) <;> simp [*]

Result:
no goals

Proof state:
case cons
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
a : β
l : List β
IH : filter p (map f l) = map f (filter (p ∘ f) l)
⊢ filter p (map f (a :: l)) = map f (filter (p ∘ f) (a :: l))

Tactic:
by_cases h : p (f a) <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem map_iInf {ι : Sort*} [Nonempty ι] (f : K →+* L) (s : ι → Subfield K) :
    (iInf s).map f = ⨅ i, (s i).map f

Proof state:
K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Result:
case a
K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Proof state:
case a
K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))

Tactic:
simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_ofList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)}
    {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (ofList l).getKey? k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (ofList l).getKey? k' = some k

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)]
lemma mulEnergy_univ_right : Eₘ[s, univ] = Fintype.card α * s.card ^ 2

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s : Finset α
⊢ Eₘ[s, univ] = Fintype.card α * #s ^ 2

Tactic:
rw [mulEnergy_comm, mulEnergy_univ_left]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem Hσ_eq_zero (q : ℕ) : (Hσ q : K[X] ⟶ K[X]).f 0 = 0

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (q + 1) 0 1 ⋯ ≫ K[X].d 1 0 = 0

Tactic:
rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ 0 = 0 + 0

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f 0 = 0

Tactic:
rw [nullHomotopicMap'_f_of_not_rel_left (c_mk 1 0 rfl) cs_down_0_not_rel_left]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' q 0 1 ⋯ ≫ K[X].d 1 0 = 0

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ hσ' 0 0 1 ⋯ ≫ K[X].d 1 0 = 0

Tactic:
rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (((-1) ^ 0 • X.σ ⟨0, ⋯⟩) ≫ eqToHom ⋯) ≫ K[X].d 1 0 = 0

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ K[X].d 1 0 = 0

Tactic:
erw [ChainComplex.of_d]

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ AlternatingFaceMapComplex.objD X 0 = 0

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ (((-1) ^ 0 • X.σ ⟨0, ⋯⟩) ≫ eqToHom ⋯) ≫ K[X].d 1 0 = 0

Tactic:
simp only [pow_zero, Fin.mk_zero, one_zsmul, eqToHom_refl, Category.comp_id]

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ K[X].d 1 0 = 0

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ X.σ 0 ≫ AlternatingFaceMapComplex.objD X 0 = 0

Tactic:
rw [AlternatingFaceMapComplex.objD, Fin.sum_univ_two, Fin.val_zero, Fin.val_one, pow_zero,
  pow_one, one_smul, neg_smul, one_smul, comp_add, comp_neg, add_neg_eq_zero,
  ← Fin.castSucc_zero, ← Fin.succ_zero_eq_one, δ_comp_σ_self, δ_comp_σ_succ]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' q 0 1 ⋯ ≫ K[X].d 1 0 = 0

Tactic:
rcases q with (_|q)

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ hσ' 0 0 1 ⋯ ≫ K[X].d 1 0 = 0

case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (q + 1) 0 1 ⋯ ≫ K[X].d 1 0 = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (Hσ q).f 0 = 0

Tactic:
unfold Hσ

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (nullHomotopicMap' (hσ' q)).f 0 = 0
-- Mathlib/Data/Int/Log.lean
theorem clog_inv (b : ℕ) (r : R) : clog b r⁻¹ = -log b r

Proof state:
case inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_right_le_one _ (inv_le_one_of_one_le₀ hr), log_of_one_le_right _ hr, inv_inv]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ clog b r⁻¹ = -log b r

Tactic:
rcases lt_or_le 0 r with hrp | hrp

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r

Proof state:
case inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
⊢ clog b r⁻¹ = -log b r

Tactic:
obtain hr | hr := le_total 1 r

Result:
case inl.inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ clog b r⁻¹ = -log b r

case inl.inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : r ≤ 0
⊢ clog b r⁻¹ = -log b r

Tactic:
rw [clog_of_right_le_zero _ (inv_nonpos.mpr hrp), log_of_right_le_zero _ hrp, neg_zero]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem Disjoint.cycleType {σ τ : Perm α} (h : Disjoint σ τ) :
    (σ * τ).cycleType = σ.cycleType + τ.cycleType

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

Tactic:
rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ←
  Multiset.map_add, Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]

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

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

Tactic:
exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_addX_of_eq {P : Fin 3 → F} (hPz : P z ≠ 0) {n d : F} (hd : d ≠ 0) :
    W.toAffine.addX (P x / P z) (P x / P z) (-n / P z / d) =
      (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z
        / (P z * d ^ 3)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * (P z * d) + -((toAffine W).a₁ * n * (P z * d) ^ 2) - (P z * d) ^ 2 * (P z * d) * (toAffine W).a₂) * P z -
            (P z * d) ^ 2 * (P z * d) * P x) *
          P z -
        (P z * d) ^ 2 * (P z * d) * P z * P x) *
      (P z * (P z * d ^ 3)) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d *
      ((P z * d) ^ 2 * (P z * d) * P z * P z)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).addX (P x / P z) (P x / P z) (-n / P z / d) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3)

Tactic:
field_simp [mul_ne_zero hPz hd]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (((n ^ 2 * (P z * d) + -((toAffine W).a₁ * n * (P z * d) ^ 2) - (P z * d) ^ 2 * (P z * d) * (toAffine W).a₂) * P z -
            (P z * d) ^ 2 * (P z * d) * P x) *
          P z -
        (P z * d) ^ 2 * (P z * d) * P z * P x) *
      (P z * (P z * d ^ 3)) =
    (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d *
      ((P z * d) ^ 2 * (P z * d) * P z * P z)
-- Mathlib/FieldTheory/IsSepClosed.lean
theorem exists_eq_mul_self [IsSepClosed k] (x : k) [h2 : NeZero (2 : k)] : ∃ z, x = z * z

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
h2 : NeZero 2
⊢ ∃ z, x = z * z

Tactic:
rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩

Result:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
h2 : NeZero 2
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1

Proof state:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
h2 : NeZero 2
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1

Tactic:
exact ⟨z, sq z⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem drop_modifyHead_of_pos {f : α → α} {l : List α} {n} (h : 0 < n) :
    (l.modifyHead f).drop n = l.drop n

Proof state:
α : Type u_1
f : α → α
l : List α
n : Nat
h : 0 < n
⊢ drop n (modifyHead f l) = drop n l

Tactic:
cases l <;> cases n <;> simp_all

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem prec' {f g h} (hf : Partrec f) (hg : Partrec g) (hh : Partrec h) :
    Partrec fun a => (f a).bind fun n => n.rec (g a)
      fun y IH => do {let i ← IH; h (Nat.pair a (Nat.pair y i))} :=
  ((prec hg hh).comp (pair Partrec.some hf)).of_eq fun a =>
    ext fun s => by simp [Seq.seq]

Proof state:
f g h : ℕ →. ℕ
hf : Partrec f
hg : Partrec g
hh : Partrec h
a s : ℕ
⊢ (s ∈
      Nat.pair <$> Part.some a <*> f a >>=
        unpaired fun a n =>
          Nat.rec (g a)
            (fun y IH => do
              let i ← IH
              h (Nat.pair a (Nat.pair y i)))
            n) ↔
    s ∈
      (f a).bind fun n =>
        Nat.rec (g a)
          (fun y IH => do
            let i ← IH
            h (Nat.pair a (Nat.pair y i)))
          n

Tactic:
simp [Seq.seq]

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem step1 (K : Subgroup G) (hK : K ⊔ N = ⊤) : K = ⊤

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
⊢ ∃ H, N.IsComplement' H

Tactic:
have h4 : (N.comap K.subtype).index = N.index := by
  rw [← N.relindex_top_right, ← hK]
  exact (relindex_sup_right K N).symm

Result:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
⊢ ∃ H, N.IsComplement' H

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
h6 : (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index
H : Subgroup ↥K
hH : Nat.card ↥(map K.subtype H) = N.index
⊢ Nat.card ↥N * Nat.card ↥(map K.subtype H) = Nat.card G

Tactic:
rw [hH, ← N.index_mul_card, mul_comm]

Result:
no goals