harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Int/Log.lean
theorem clog_of_right_le_zero (b : ℕ) {r : R} (hr : r ≤ 0) : clog b r = 0

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1

Tactic:
exact Nat.floor_le_one_of_le_one ((inv_nonpos.2 hr).trans zero_le_one)

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
exact Or.inr hb

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ clog b r = 0

Tactic:
rw [clog, if_neg (hr.trans_lt zero_lt_one).not_le, neg_eq_zero, Int.natCast_eq_zero,
  Nat.log_eq_zero_iff]

Result:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
rcases le_or_lt b 1 with hb | hb

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : b ≤ 1
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
refine Or.inl (lt_of_le_of_lt ?_ hb)

Result:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1
-- Mathlib/GroupTheory/CoprodI.lean
theorem inv_last {i j} (w : NeWord G i j) : w.inv.last = w.head⁻¹

Proof state:
ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Group (G i)
i j : ι
w : NeWord G i j
⊢ w.inv.last = w.head⁻¹

Tactic:
induction w <;> simp [inv, *]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem range_succ (n : Nat) : range (succ n) = range n ++ #v[n]

Proof state:
n : Nat
⊢ range n.succ = range n ++ { toArray := #[n], size_toArray := ⋯ }

Tactic:
rw [← toArray_inj]

Result:
n : Nat
⊢ (range n.succ).toArray = (range n ++ { toArray := #[n], size_toArray := ⋯ }).toArray

Proof state:
n : Nat
⊢ (range n.succ).toArray = (range n ++ { toArray := #[n], size_toArray := ⋯ }).toArray

Tactic:
simp [Array.range_succ]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_mul' {p q : ℝ} (hq : 0 ≤ q) :
    ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

Proof state:
p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q

Tactic:
rw [mul_comm, ofReal_mul hq, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem hcongr_hom {F G : C ⥤ D} (h : F = G) {X Y} (f : X ⟶ Y) : HEq (F.map f) (G.map f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ HEq (F.map f) (G.map f)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem congr_symm_tprod (f : Π i, s i ≃ₗ[R] t i) (p : Π i, t i) :
    (congr f).symm (tprod R p) = tprod R (fun (i : ι) ↦ (f i).symm (p i))

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i ≃ₗ[R] t i
p : (i : ι) → t i
⊢ (congr f).symm ((tprod R) p) = ⨂ₜ[R] (i : ι), (f i).symm (p i)

Tactic:
simp only [congr, LinearEquiv.ofLinear_symm_apply, map_tprod, LinearEquiv.coe_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_singleton (a : α) : countP p #[a] = if p a then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
⊢ countP p #[a] = if p a = true then 1 else 0

Tactic:
simp [countP_push]

Result:
no goals
-- Mathlib/LinearAlgebra/Trace.lean
theorem trace_one : trace R M 1 = (finrank R M : R)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (trace R M) 1 = ↑(finrank R M)

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
⊢ (trace R M) 1 = ↑(finrank R M)

case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
⊢ (trace R M) 1 = ↑(finrank R M)

Proof state:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
⊢ (trace R M) 1 = ↑(finrank R M)

Tactic:
have b := Module.Free.chooseBasis R M

Result:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ (trace R M) 1 = ↑(finrank R M)

Proof state:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ (trace R M) 1 = ↑(finrank R M)

Tactic:
rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]

Result:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(Fintype.card (Free.ChooseBasisIndex R M))

Proof state:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(Fintype.card (Free.ChooseBasisIndex R M))

Tactic:
simp

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
⊢ (trace R M) 1 = ↑(finrank R M)

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_mul_single_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
    (f * single a r).support ⊆ Finset.image (· * a) f.support :=
  (support_mul _ _).trans <| (Finset.image₂_subset_left support_single_subset).trans <| by
    rw [Finset.image₂_singleton_right]

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a : G
⊢ image₂ (fun x1 x2 => x1 * x2) f.support {a} ⊆ image (fun x => x * a) f.support

Tactic:
rw [Finset.image₂_singleton_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_eq_fallback [EquivBEq α] [LawfulHashable α] (h : m.WF) {a fallback : α} :
    ¬a ∈ m → m.getKeyD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
a fallback : α
⊢ ¬a ∈ m → m.getKeyD a fallback = fallback

Tactic:
simpa [mem_iff_contains] using getKeyD_eq_fallback_of_contains_eq_false h

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
@[simp]
lemma ShortComplex.zero_apply
    [Limits.HasZeroMorphisms C] [(forget₂ C Ab).PreservesZeroMorphisms]
    (S : ShortComplex C) (x : (forget₂ C Ab).obj S.X₁) :
    ((forget₂ C Ab).map S.g) (((forget₂ C Ab).map S.f) x) = 0

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom 0) x = 0

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) ((ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x) = 0

Tactic:
rw [← ConcreteCategory.comp_apply, ← Functor.map_comp, S.zero, Functor.map_zero]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom 0) x = 0
-- Mathlib/Order/Defs/LinearOrder.lean
lemma min_left_comm (a b c : α) : min a (min b c) = min b (min a c)

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ min a (min b c) = min b (min a c)

Tactic:
rw [← min_assoc, min_comm a, min_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem extract_mk (a : Array α) (h : a.size = n) (start stop) :
    (Vector.mk a h).extract start stop = Vector.mk (a.extract start stop) (by simp [h]) := rfl

Proof state:
α : Type ?u.8447
n : Nat
a : Array α
h : a.size = n
start stop : Nat
⊢ (a.extract start stop).size = min stop n - start

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma range_snd_comp :
    Set.range (pullback.snd f g ≫ g).base = Set.range f.base ∩ Set.range g.base

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g ≫ g).base) =
    Set.range ⇑(ConcreteCategory.hom f.base) ∩ Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
rw [← pullback.condition, range_fst_comp]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_tsub_tsub_cancel_left (hab : AddLECancellable (a - b)) (h : b ≤ a) :
    a - c - (a - b) = b - c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h : b ≤ a
⊢ a - c - (a - b) = b - c

Tactic:
rw [tsub_right_comm, hab.tsub_tsub_cancel_of_le h]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma subset_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    ↑(hC.disjointOfDiff hs ht) ⊆ C

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ↑⋯.choose ⊆ insert ∅ C

Tactic:
exact (hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ↑(hC.disjointOfDiff hs ht) ⊆ C

Tactic:
classical
simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
exact (hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ↑(hC.disjointOfDiff hs ht) ⊆ C

Tactic:
simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ↑⋯.choose ⊆ insert ∅ C
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_concat_self (a : α) (l : List α) :
    count a (concat l a) = (count a l) + 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ count a (l.concat a) = count a l + 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ l.all p = true ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp only [← all_toList, List.all_eq_true, mem_def]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.disjoint_iff (hl : l.HasBasis p s) (hl' : l'.HasBasis p' s') :
    Disjoint l l' ↔ ∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i') :=
  not_iff_not.mp <| by simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter,
    hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
⊢ ¬Disjoint l l' ↔ ¬∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')

Tactic:
simp only [_root_.disjoint_iff, ← Ne.eq_def, ← neBot_iff, inf_eq_inter,
hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[simp]
lemma shiftFunctorComm_eq_refl (i : A) :
    shiftFunctorComm C i i = Iso.refl _

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i : A
⊢ shiftFunctorComm C i i = Iso.refl (shiftFunctor C i ⋙ shiftFunctor C i)

Tactic:
rw [shiftFunctorComm_eq C i i (i + i) rfl, Iso.symm_self_id]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndepOn_id_insert (hxs : x ∉ s) :
    LinearIndepOn K id (insert x s) ↔ LinearIndepOn K id s ∧ x ∉ Submodule.span K s :=
  (linearIndepOn_insert (f := id) hxs).trans <| by simp

Proof state:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
x : V
hxs : x ∉ s
⊢ LinearIndepOn K id s ∧ id x ∉ span K (id '' s) ↔ LinearIndepOn K id s ∧ x ∉ span K s

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem comap_subtype_eq_top {p p' : Submodule R M} : comap p.subtype p' = ⊤ ↔ p ≤ p' :=
  eq_top_iff.trans <| map_le_iff_le_comap.symm.trans <| by rw [map_subtype_top]

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
⊢ map p.subtype ⊤ ≤ p' ↔ p ≤ p'

Tactic:
rw [map_subtype_top]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma one_le_star_iff {x : R} : 1 ≤ star x ↔ 1 ≤ x

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 1 ≤ star x ↔ 1 ≤ x

Tactic:
simpa using star_le_star_iff (x := 1) (y := x)

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem le_iterate_pos_iff {x : ℝ} {m : ℤ} {n : ℕ} (hn : 0 < n) :
    x + n * m ≤ f^[n] x ↔ x + m ≤ f x

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x

Tactic:
simpa only [not_lt] using not_congr (f.iterate_pos_lt_iff hn)

Result:
no goals
-- Mathlib/RingTheory/WittVector/Frobenius.lean
theorem frobeniusPoly_zmod (n : ℕ) :
    MvPolynomial.map (Int.castRingHom (ZMod p)) (frobeniusPoly p n) = X n ^ p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p + C ((Int.castRingHom (ZMod p)) ↑p) * (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) =
    X n ^ p

Tactic:
simp only [Int.cast_natCast, add_zero, eq_intCast, ZMod.natCast_self, zero_mul, C_0]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPoly p n) = X n ^ p

Tactic:
rw [frobeniusPoly, RingHom.map_add, RingHom.map_pow, RingHom.map_mul, map_X, map_C]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p + C ((Int.castRingHom (ZMod p)) ↑p) * (MvPolynomial.map (Int.castRingHom (ZMod p))) (frobeniusPolyAux p n) =
    X n ^ p
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem sign_kerParam_apply_apply :
    sign (kerParam g ⟨k, v⟩) = sign k * ∏ c, sign (v c).val

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
⊢ sign ((kerParam g) (k, v)) = sign k * ∏ c : { x // x ∈ g.cycleFactorsFinset }, sign ↑(v c)

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one,
  one_mul, map_mul, sign_ofSubtype, Finset.univ_eq_attach, mul_right_inj, ← MonoidHom.comp_apply,
  Subgroup.noncommPiCoprod, MonoidHom.comp_noncommPiCoprod _, MonoidHom.noncommPiCoprod_apply,
  Finset.univ_eq_attach, Finset.noncommProd_eq_prod]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
⊢ ∏ i ∈ g.cycleFactorsFinset.attach, (sign.comp (zpowers ↑i).subtype) (((k, v).1, (k, v).2).2 i) =
    ∏ c ∈ g.cycleFactorsFinset.attach, sign ↑(v c)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
k : Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c)
⊢ ∏ i ∈ g.cycleFactorsFinset.attach, (sign.comp (zpowers ↑i).subtype) (((k, v).1, (k, v).2).2 i) =
    ∏ c ∈ g.cycleFactorsFinset.attach, sign ↑(v c)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Category/BddDistLat.lean
lemma hom_inv_apply {X Y : BddDistLat} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : BddDistLat
e : X ≅ Y
s : ↑Y.toDistLat
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_norm_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : R}
    (hr : ‖r‖ < 1) : Summable fun n : ℕ ↦ ‖((n : R) ^ k * r ^ n : R)‖

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ‖↑(n ^ k) * r ^ n‖

Tactic:
exact summable_norm_mul_geometric_of_norm_lt_one (k := k) (u := fun n ↦ n ^ k) hr
  (isBigO_refl _ _)

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ‖↑n ^ k * r ^ n‖

Tactic:
simp only [← cast_pow]

Result:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
⊢ Summable fun n => ‖↑(n ^ k) * r ^ n‖
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_add_nat (a : α) (n : ℕ) : ⌊a + n⌋ = ⌊a⌋ + n

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
n : ℕ
⊢ ⌊a + ↑n⌋ = ⌊a⌋ + ↑n

Tactic:
rw [← Int.cast_natCast, floor_add_int]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem induced_to_pi {X : Type*} (f : X → ∀ i, π i) :
    induced f Pi.topologicalSpace = ⨅ i, induced (f · i) inferInstance

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
X : Type u_8
f : X → (i : ι) → π i
⊢ induced f Pi.topologicalSpace = ⨅ i, induced (fun x => f x i) inferInstance

Tactic:
simp_rw [Pi.topologicalSpace, induced_iInf, induced_compose, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Countable/Basic.lean
theorem uncountable_iff_isEmpty_embedding : Uncountable α ↔ IsEmpty (α ↪ ℕ)

Proof state:
α : Sort u
⊢ Uncountable α ↔ IsEmpty (α ↪ ℕ)

Tactic:
rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_push_size {a : Vector α n} {x} : (a.push x)[n]? = some x

Proof state:
α : Type u_1
n : Nat
a : Vector α n
x : α
⊢ (a.push x)[n]? = some x

Tactic:
simp [getElem?_push]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Ici_mul_Ioi_subset' [LocallyFiniteOrderTop α] (a b : α) : Ici a * Ioi b ⊆ Ioi (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Ici_mul_Ioi_subset' _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrderTop α
a b : α
⊢ ↑(Ici a * Ioi b) ⊆ ↑(Ioi (a * b))

Tactic:
simpa using Set.Ici_mul_Ioi_subset' _ _

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_eq_zero_or_eq_pi_iff_collinear {p₁ p₂ p₃ : P} :
    ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = π ↔ Collinear ℝ ({p₁, p₂, p₃} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ = 0 ∨ ∡ p₁ p₂ p₃ = ↑π ↔ Collinear ℝ {p₁, p₂, p₃}

Tactic:
rw [← not_iff_not, not_or, oangle_ne_zero_and_ne_pi_iff_affineIndependent,
  affineIndependent_iff_not_collinear_set]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem findSomeM?_toArray [Monad m] (f : α → m (Option β)) (v : Vector α n) :
    v.toArray.findSomeM? f = v.findSomeM? f

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝ : Monad m
f : α → m (Option β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝ : Monad m
f : α → m (Option β)
v : Vector α n
⊢ Array.findSomeM? f v.toArray = findSomeM? f v

Tactic:
cases v

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝ : Monad m
f : α → m (Option β)
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ Array.findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray =
    findSomeM? f { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem isAlgebraic_algHom_iff (f : A →ₐ[R] B) (hf : Function.Injective f)
    {a : A} : IsAlgebraic R (f a) ↔ IsAlgebraic R a :=
  ⟨fun ⟨p, hp0, hp⟩ ↦ ⟨p, hp0, hf <| by rwa [map_zero, ← f.comp_apply, ← aeval_algHom]⟩,
    IsAlgebraic.algHom f⟩

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
a : A
x✝ : IsAlgebraic R (f a)
p : R[X]
hp0 : p ≠ 0
hp : (aeval (f a)) p = 0
⊢ f ((aeval a) p) = f 0

Tactic:
rwa [map_zero, ← f.comp_apply, ← aeval_algHom]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.xor_left_inj (a b c : BitVec w) : (a ^^^ c == b ^^^ c) = (a == b)

Proof state:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = (a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b c : BitVec w
⊢ (a ^^^ c == b ^^^ c) = true ↔ (a == b) = true
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lTensor_comp_apply (x : M ⊗[R] N) :
    (g.comp f).lTensor M x = (g.lTensor M) ((f.lTensor M) x)

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ (⇑(lTensor M g) ∘ ⇑(lTensor M f)) x = (lTensor M g) ((lTensor M f) x)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ (lTensor M (g ∘ₗ f)) x = (lTensor M g) ((lTensor M f) x)

Tactic:
rw [lTensor_comp, coe_comp]

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
g : P →ₗ[R] Q
f : N →ₗ[R] P
x : M ⊗[R] N
⊢ (⇑(lTensor M g) ∘ ⇑(lTensor M f)) x = (lTensor M g) ((lTensor M f) x)