harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem map_comp_map (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) :
    (map f).comp (map g) = map (f.comp g)

Proof state:
case a.h
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((map g) ((ι Q₁) m)) = (map (f.comp g)) ((ι Q₁) m)

Tactic:
rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
⊢ (map f).comp (map g) = map (f.comp g)

Tactic:
ext m

Result:
case a.h
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (((map f).comp (map g)).toLinearMap ∘ₗ ι Q₁) m = ((map (f.comp g)).toLinearMap ∘ₗ ι Q₁) m

Proof state:
case a.h
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (((map f).comp (map g)).toLinearMap ∘ₗ ι Q₁) m = ((map (f.comp g)).toLinearMap ∘ₗ ι Q₁) m

Tactic:
dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]

Result:
case a.h
R : Type u_1
inst✝⁶ : CommRing R
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
f : Q₂ →qᵢ Q₃
g : Q₁ →qᵢ Q₂
m : M₁
⊢ (map f) ((map g) ((ι Q₁) m)) = (map (f.comp g)) ((ι Q₁) m)
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem card_opow_le_of_omega0_le_right (a : Ordinal) {b : Ordinal} (hb : ω ≤ b) :
    (a ^ b).card ≤ max a.card b.card

Proof state:
a b : Ordinal.{u_1}
hb : ω ≤ b
⊢ (a ^ b).card ≤ a.card ⊔ b.card

Tactic:
obtain ⟨n, rfl⟩ | ha := eq_nat_or_omega0_le a

Result:
case inl.intro
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (↑n ^ b).card ≤ (↑n).card ⊔ b.card

case inr
a b : Ordinal.{u_1}
hb : ω ≤ b
ha : ω ≤ a
⊢ (a ^ b).card ≤ a.card ⊔ b.card

Proof state:
case inl.intro
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ ω.card ⊔ b.card ≤ (↑n).card ⊔ b.card

Tactic:
simp [hb]

Result:
no goals

Proof state:
case inl.intro
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (↑n ^ b).card ≤ (↑n).card ⊔ b.card

Tactic:
apply (card_le_card <| opow_le_opow_left b (nat_lt_omega0 n).le).trans

Result:
case inl.intro
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (ω ^ b).card ≤ (↑n).card ⊔ b.card

Proof state:
case inl.intro
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (ω ^ b).card ≤ (↑n).card ⊔ b.card

Tactic:
apply (card_opow_le_of_omega0_le_left le_rfl _).trans

Result:
case inl.intro
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ ω.card ⊔ b.card ≤ (↑n).card ⊔ b.card

Proof state:
case inr
a b : Ordinal.{u_1}
hb : ω ≤ b
ha : ω ≤ a
⊢ (a ^ b).card ≤ a.card ⊔ b.card

Tactic:
exact card_opow_le_of_omega0_le_left ha b

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma rpow_neg_one_le_rpow_neg_one {a b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hau : IsUnit a) :
    b ^ (-1 : ℝ) ≤ a ^ (-1 : ℝ)

Proof state:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
hau : IsUnit a
b : Aˣ
hab : a ≤ ↑b
⊢ ↑b ^ (-1) ≤ a ^ (-1)

Tactic:
lift a to Aˣ using hau

Result:
case intro.intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
⊢ ↑b ^ (-1) ≤ ↑a ^ (-1)

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
ha : 0 ≤ a
hab : a ≤ b
hau : IsUnit a
⊢ b ^ (-1) ≤ a ^ (-1)

Tactic:
lift b to Aˣ using isUnit_of_le hau ha hab

Result:
case intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : 0 ≤ a
hau : IsUnit a
b : Aˣ
hab : a ≤ ↑b
⊢ ↑b ^ (-1) ≤ a ^ (-1)

Proof state:
case intro.intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
⊢ ↑b ^ (-1) ≤ ↑a ^ (-1)

Tactic:
rw [rpow_neg_one_eq_inv a ha, rpow_neg_one_eq_inv b (ha.trans hab)]

Result:
case intro.intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Proof state:
case intro.intro
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
b a : Aˣ
ha : 0 ≤ ↑a
hab : ↑a ≤ ↑b
⊢ ↑b⁻¹ ≤ ↑a⁻¹

Tactic:
exact CStarAlgebra.inv_le_inv ha hab

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_bisim_tail {ys : Vector β n} {f₁ : α → β → σ₁ → σ₁ × γ}
    {f₂ : α → β → σ₂ → σ₂ × γ} {s₁ : σ₁} {s₂ : σ₂}
    (h : ∃ R : σ₁ → σ₂ → Prop, R s₁ s₂ ∧
      ∀ {s q} a b, R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2) :
    (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
h :
  ∃ R, R s₁ s₂ ∧ ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
rcases h with ⟨R, h₀, hR⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
ys : Vector β n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
s₁ : σ₁
s₂ : σ₂
R : σ₁ → σ₂ → Prop
h₀ : R s₁ s₂
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
⊢ (mapAccumr₂ f₁ xs ys s₁).2 = (mapAccumr₂ f₂ xs ys s₂).2

Tactic:
exact (mapAccumr₂_bisim R h₀ hR).2

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_simpleFunc_indicatorConst (hT : DominatedFinMeasAdditive μ T C) {s : Set α}
    (hs : MeasurableSet s) (hμs : μ s < ∞) (x : E) :
    setToL1 hT (simpleFunc.indicatorConst 1 hs hμs.ne x) = T s x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
x : E
⊢ (setToL1 hT) ↑(indicatorConst 1 hs ⋯ x) = (T s) x

Tactic:
rw [setToL1_eq_setToL1SCLM]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
x : E
⊢ (setToL1SCLM α E μ hT) (indicatorConst 1 hs ⋯ x) = (T s) x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
x : E
⊢ (setToL1SCLM α E μ hT) (indicatorConst 1 hs ⋯ x) = (T s) x

Tactic:
exact setToL1S_indicatorConst (fun s => hT.eq_zero_of_measure_zero) hT.1 hs hμs x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_add (x : BitVec n) : 0#n + x = x

Proof state:
n : Nat
x : BitVec n
⊢ 0#n + x = x

Tactic:
simp [add_def]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem associative_of_commutative_of_le {f : α → α → α} (comm : Std.Commutative f)
    (assoc : ∀ a b c, f (f a b) c ≤ f a (f b c)) : Std.Associative f where
  assoc a b c :=
    le_antisymm (assoc _ _ _) <| by
      rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]
      exact assoc _ _ _

Proof state:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c

Tactic:
rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]

Result:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)

Proof state:
α : Type u_2
inst✝ : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f (f c b) a ≤ f c (f b a)

Tactic:
exact assoc _ _ _

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_comm {β'} {f : β ↪ γ} {g : α ↪ β} {f' : α ↪ β'} {g' : β' ↪ γ}
    (h_comm : ∀ a, f (g a) = g' (f' a)) : (s.map g).map f = (s.map f').map g'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ map f (map g s) = map g' (map f' s)

Tactic:
simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_mul_left (h : H) (g : G) :
    hHT.equiv (h * g) = (h * (hHT.equiv g).fst, (hHT.equiv g).snd)

Proof state:
case refine_2.fst.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).1 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).1

Tactic:
rw [coe_mul, equiv_fst_eq_mul_inv, this, equiv_fst_eq_mul_inv, mul_assoc]

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
⊢ RightCosetEquivalence (↑H) (↑h * g) g

Tactic:
simp [RightCosetEquivalence, ← smul_smul]

Result:
no goals

Proof state:
case refine_2.snd.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).2 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).2

Tactic:
rw [this]

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)

Tactic:
ext

Result:
case refine_2.fst.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).1 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).1

case refine_2.snd.a
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ ↑(hHT.equiv (↑h * g)).2 = ↑(h * (hHT.equiv g).1, (hHT.equiv g).2).2

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
⊢ hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)

Tactic:
have : (hHT.equiv (h * g)).2 = (hHT.equiv g).2 := hHT.equiv_snd_eq_iff_rightCosetEquivalence.2 ?_

Result:
case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
this : (hHT.equiv (↑h * g)).2 = (hHT.equiv g).2
⊢ hHT.equiv (↑h * g) = (h * (hHT.equiv g).1, (hHT.equiv g).2)

case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
T : Set G
hHT : IsComplement (↑H) T
h : ↥H
g : G
⊢ RightCosetEquivalence (↑H) (↑h * g) g
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_mul_le {p q : R[X]} : natDegree (p * q) ≤ natDegree p + natDegree q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).natDegree ≤ p.natDegree + q.natDegree

Tactic:
apply natDegree_le_of_degree_le

Result:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).degree ≤ ↑(p.natDegree + q.natDegree)

Proof state:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑p.natDegree + ↑q.natDegree

Tactic:
apply add_le_add <;> apply degree_le_natDegree

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).degree ≤ ↑(p.natDegree + q.natDegree)

Tactic:
apply le_trans (degree_mul_le p q)

Result:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑(p.natDegree + q.natDegree)

Proof state:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑(p.natDegree + q.natDegree)

Tactic:
rw [Nat.cast_add]

Result:
case a
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑p.natDegree + ↑q.natDegree
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_injective {H : Type*} [Monoid H] (f : G →* H) (hf : Function.Injective f) (x : G) :
    orderOf (f x) = orderOf x

Proof state:
G : Type u_1
inst✝¹ : Monoid G
H : Type u_6
inst✝ : Monoid H
f : G →* H
hf : Injective ⇑f
x : G
⊢ orderOf (f x) = orderOf x

Tactic:
simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertMany_nil [EquivBEq α] [LawfulHashable α] (h : m.WF) :
    m.insertMany [] = m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ m.insertMany [] = m

Tactic:
simp_to_raw

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ (Raw₀.insertMany ⟨m, ⋯⟩ []).val.val = m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
⊢ (Raw₀.insertMany ⟨m, ⋯⟩ []).val.val = m

Tactic:
rw [Raw₀.insertMany_nil]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
lemma growsPolynomially_const {c : ℝ} : GrowsPolynomially (fun _ => c)

Proof state:
c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
⊢ 1 > 0

Tactic:
norm_num

Result:
no goals

Proof state:
case h
c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
x : ℝ
⊢ ∀ u ∈ Set.Icc (x✝¹ * x) x, c ∈ Set.Icc (1 * c) (1 * c)

Tactic:
simp

Result:
no goals

Proof state:
c : ℝ
⊢ GrowsPolynomially fun x => c

Tactic:
refine fun _ _ => ⟨1, by norm_num, 1, by norm_num, ?_⟩

Result:
c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (x✝¹ * x) x, (fun x => c) u ∈ Set.Icc (1 * (fun x => c) x) (1 * (fun x => c) x)

Proof state:
c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (x✝¹ * x) x, (fun x => c) u ∈ Set.Icc (1 * (fun x => c) x) (1 * (fun x => c) x)

Tactic:
filter_upwards [] with x

Result:
case h
c x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.Ioo 0 1
x : ℝ
⊢ ∀ u ∈ Set.Icc (x✝¹ * x) x, c ∈ Set.Icc (1 * c) (1 * c)
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem hom_cast_eq_of_cons_eq_cons {u v v' w : U} {p : Path u v} {p' : Path u v'} {e : v ⟶ w}
    {e' : v' ⟶ w} (h : p.cons e = p'.cons e') : e.cast (obj_eq_of_cons_eq_cons h) rfl = e'

Proof state:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
rw [Hom.cast_eq_iff_heq]

Result:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ HEq e e'

Proof state:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ HEq e e'

Tactic:
exact hom_heq_of_cons_eq_cons h

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) addConst_mul_card]
lemma mulConst_mul_card (A B : Finset G) : σₘ[A, B] * #A = #(A * B)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ ↑(#A) ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] * ↑(#∅) = ↑(#(∅ * B))

Tactic:
simp

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
exact div_mul_cancel₀ _ (by positivity)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Result:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] * ↑(#∅) = ↑(#(∅ * B))

case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
hA : A.Nonempty
⊢ σₘ[A, B] * ↑(#A) = ↑(#(A * B))
-- Mathlib/Data/Int/GCD.lean
theorem pow_dvd_pow_iff {m n : ℤ} {k : ℕ} (k0 : k ≠ 0) : m ^ k ∣ n ^ k ↔ m ∣ n

Proof state:
m n : ℤ
k : ℕ
k0 : k ≠ 0
h : m ^ k ∣ n ^ k
⊢ m ∣ n

Tactic:
rwa [← natAbs_dvd_natAbs, ← Nat.pow_dvd_pow_iff k0, ← Int.natAbs_pow, ← Int.natAbs_pow,
  natAbs_dvd_natAbs]

Result:
no goals

Proof state:
m n : ℤ
k : ℕ
k0 : k ≠ 0
⊢ m ^ k ∣ n ^ k ↔ m ∣ n

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

Result:
m n : ℤ
k : ℕ
k0 : k ≠ 0
h : m ^ k ∣ n ^ k
⊢ m ∣ n
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_single {f : β → α} (b : β) (hf : ∀ (b') (_ : b' ≠ b), f b' = 1) : HasProd f (f b) :=
  suffices HasProd f (∏ b' ∈ {b}, f b') by simpa using this
  hasProd_prod_of_ne_finset_one <| by simpa [hf]

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1

Tactic:
simpa [hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
this : HasProd f (∏ b' ∈ {b}, f b')
⊢ HasProd f (f b)

Tactic:
simpa using this

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem iSup_principal {ι : Sort w} {s : ι → Set α} : ⨆ x, 𝓟 (s x) = 𝓟 (⋃ i, s i) :=
  Filter.ext fun x => by simp only [mem_iSup, mem_principal, iUnion_subset_iff]

Proof state:
α : Type u
ι : Sort w
s : ι → Set α
x : Set α
⊢ x ∈ ⨆ x, 𝓟 (s x) ↔ x ∈ 𝓟 (⋃ i, s i)

Tactic:
simp only [mem_iSup, mem_principal, iUnion_subset_iff]

Result:
no goals
-- Mathlib/Topology/Category/CompHausLike/Limits.lean
lemma finiteCoproduct.ι_desc_apply {B : CompHausLike P} {π : (a : α) → X a ⟶ B} (a : α) :
    ∀ x, finiteCoproduct.desc X π (finiteCoproduct.ι X a x) = π a x

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom (desc X π)) ((ConcreteCategory.hom (ι X a)) x) = (ConcreteCategory.hom (π a)) x

Tactic:
change (ι X a ≫ desc X π) _ = _

Result:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom (ι X a ≫ desc X π)) x = (ConcreteCategory.hom (π a)) x

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom (ι X a ≫ desc X π)) x = (ConcreteCategory.hom (π a)) x

Tactic:
simp only [ι_desc]

Result:
no goals

Proof state:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
⊢ ∀ (x : (fun X => ↑X.toTop) (X a)),
    (ConcreteCategory.hom (desc X π)) ((ConcreteCategory.hom (ι X a)) x) = (ConcreteCategory.hom (π a)) x

Tactic:
intro x

Result:
P : TopCat → Prop
α : Type w
inst✝¹ : Finite α
X : α → CompHausLike P
inst✝ : HasExplicitFiniteCoproduct X
B : CompHausLike P
π : (a : α) → X a ⟶ B
a : α
x : ↑(X a).toTop
⊢ (ConcreteCategory.hom (desc X π)) ((ConcreteCategory.hom (ι X a)) x) = (ConcreteCategory.hom (π a)) x
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma mk₀_id_comp (α : Ext X Y n) :
    (mk₀ (𝟙 X)).comp α (zero_add n) = α

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
⊢ (mk₀ (𝟙 X)).comp α ⋯ = α

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ (𝟙 X)).comp α ⋯ = α

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ (𝟙 X)).comp α ⋯ = α

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((mk₀ (𝟙 X)).comp α ⋯).hom = α.hom

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((mk₀ (𝟙 X)).comp α ⋯).hom = α.hom

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SmoothingSeminorm.lean
theorem smoothingFun_le_self (x : R) : smoothingFun μ x ≤ μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ smoothingFun μ x ≤ μ x

Tactic:
apply (smoothingFun_le μ x 1).trans

Result:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ μ (x ^ ↑1) ^ (1 / ↑↑1) ≤ μ x

Proof state:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
x : R
⊢ μ (x ^ ↑1) ^ (1 / ↑↑1) ≤ μ x

Tactic:
rw [PNat.one_coe, pow_one, cast_one, div_one, rpow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) : n = k

Proof state:
n m k : Nat
hm : 0 < m
h : m * n = m * k
⊢ n = k

Tactic:
exact Nat.eq_of_mul_eq_mul_left hm h

Result:
no goals

Proof state:
n m k : Nat
hm : 0 < m
h : n * m = k * m
⊢ n = k

Tactic:
rw [Nat.mul_comm n m, Nat.mul_comm k m] at h

Result:
n m k : Nat
hm : 0 < m
h : m * n = m * k
⊢ n = k
-- Mathlib/Probability/Martingale/Convergence.lean
theorem not_frequently_of_upcrossings_lt_top (hab : a < b) (hω : upcrossings a b f ω ≠ ∞) :
    ¬((∃ᶠ n in atTop, f n ω < a) ∧ ∃ᶠ n in atTop, b < f n ω)

Proof state:
case intro.zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b ≥ a_1, f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1 ≥ a, b < f b_1 ω
⊢ ∃ N, 0 ≤ upcrossingsBefore a b f N ω

Tactic:
simp only [zero_le, exists_const]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_neg {R : Type u} [Ring R] (a : R[X]) : (-a).toFinsupp = -a.toFinsupp

Proof state:
case ofFinsupp
R : Type u
inst✝ : Ring R
toFinsupp✝ : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp

Tactic:
rw [← ofFinsupp_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
a : R[X]
⊢ (-a).toFinsupp = -a.toFinsupp

Tactic:
cases a

Result:
case ofFinsupp
R : Type u
inst✝ : Ring R
toFinsupp✝ : R[ℕ]
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp