harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Subring/Defs.lean
theorem intCast_mem (n : ℤ) : (n : R) ∈ s

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : SetLike S R
hSR : SubringClass S R
s : S
n : ℤ
⊢ ↑n ∈ s

Tactic:
simp only [← zsmul_one, zsmul_mem, one_mem]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem coeff_one (k : ℕ) : k.rawCast = (nat_lit 1).rawCast * k

Proof state:
k : ℕ
⊢ k.rawCast = Nat.rawCast 1 * k

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem sub_submartingale [Preorder E] [AddLeftMono E]
    (hf : Supermartingale f ℱ μ) (hg : Submartingale g ℱ μ) : Supermartingale (f - g) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f - g) ℱ μ

Tactic:
rw [sub_eq_add_neg]

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f + -g) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Supermartingale (f + -g) ℱ μ

Tactic:
exact hf.add hg.neg

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem preimage_mul_right_singleton :
    preimage {b} (· * a) (mul_left_injective _).injOn = {b * a⁻¹}

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x => x * a) ⋯ = {b * a⁻¹}

Tactic:
classical rw [← image_mul_right', image_singleton]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x => x * a) ⋯ = {b * a⁻¹}

Tactic:
rw [← image_mul_right', image_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_filter_le (p : α → Bool) (l : Array α) :
    (l.filter p).size ≤ l.size

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p { toList := l }).size ≤ { toList := l }.size

Tactic:
simpa using List.length_filter_le p l

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).size ≤ l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ (filter p { toList := l }).size ≤ { toList := l }.size
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem CokernelCofork.π_eq_zero (s : CokernelCofork f) : s.ι.app zero = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : CokernelCofork f
⊢ s.ι.app zero = 0

Tactic:
simp [Cofork.app_zero_eq_comp_π_right]

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem iselect_cons [DecidableEq F.A] [Inhabited (M F)] (ps : Path F) {a} (f : F.B a → M F) {i} :
    iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i)

Proof state:
F : PFunctor.{u}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect ps (f i)

Tactic:
simp only [iselect, isubtree_cons]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Bounded.weak_right : ∀ {t : Ordnode α} {o₁ o₂}, Bounded t o₁ o₂ → Bounded t o₁ ⊤
  | nil, o₁, o₂, h => by cases o₁ <;> trivial
  | node _ _ _ _, _, _, ⟨ol, Or⟩ => ⟨ol, Or.weak_right⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : nil.Bounded o₁ o₂
⊢ nil.Bounded o₁ ⊤

Tactic:
cases o₁ <;> trivial

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_sub_eq_sub (a b c : α) : toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocMod hp a (b - c) = toIocMod hp (a + c) b - c

Tactic:
simp_rw [toIocMod, toIocDiv_sub_eq_toIocDiv_add, sub_right_comm]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_coe (P : Polynomial F) : ((P : F⟦X⟧) : F⸨X⸩) = (P : RatFunc F)

Proof state:
F : Type u
inst✝ : Field F
P : F[X]
⊢ (ofPowerSeries ℤ F) ↑P = ↑↑P

Tactic:
simp only [coePolynomial, coe_def, AlgHom.commutes, algebraMap_hahnSeries_apply]

Result:
no goals
-- Mathlib/Analysis/Normed/MulAction.lean
theorem dist_smul_le (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y

Tactic:
simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Filter.HasBasis.cauchy_iff {ι} {p : ι → Prop} {s : ι → Set (α × α)} (h : (𝓤 α).HasBasis p s)
    {f : Filter α} :
    Cauchy f ↔ NeBot f ∧ ∀ i, p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i :=
  and_congr Iff.rfl <|
    (f.basis_sets.prod_self.le_basis_iff h).trans <| by
      simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Proof state:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
p : ι → Prop
s : ι → Set (α × α)
h : (𝓤 α).HasBasis p s
f : Filter α
⊢ (∀ (i' : ι), p i' → ∃ i ∈ f, id i ×ˢ id i ⊆ s i') ↔ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i

Tactic:
simp only [subset_def, Prod.forall, mem_prod_eq, and_imp, id, forall_mem_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_zip (as : Array α) (bs : Array β) :
    (zip as bs).toList = List.zip as.toList bs.toList

Proof state:
α : Type u_1
β : Type u_2
as : Array α
bs : Array β
⊢ (as.zip bs).toList = as.toList.zip bs.toList

Tactic:
simp [zip, toList_zipWith, List.zip]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} : m.isEmpty = true → m.get? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
⊢ m.isEmpty = true → m.get? a = none

Tactic:
simp_to_raw using Raw₀.get?_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Canonical.lean
lemma tsub_one_mul [MulRightMono α] [AddLeftReflectLE α] (a b : α) :
    (a - 1) * b = a * b - b

Proof state:
α : Type u
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : PartialOrder α
inst✝⁵ : CanonicallyOrderedAdd α
inst✝⁴ : Sub α
inst✝³ : OrderedSub α
inst✝² : IsTotal α fun x1 x2 => x1 ≤ x2
inst✝¹ : MulRightMono α
inst✝ : AddLeftReflectLE α
a b : α
⊢ (a - 1) * b = a * b - b

Tactic:
rw [tsub_mul, one_mul]

Result:
no goals
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_cons_right (b a : α) (s : Multiset α) : (a ::ₘ s).fold op b = s.fold op b * a

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b a : α
s : Multiset α
⊢ fold op b (a ::ₘ s) = op (fold op b s) a

Tactic:
simp [hc.comm]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem tendsto_nhds_atTop_iff [Preorder β] {l : Filter α} {f : α → Filter β} :
    Tendsto f l (𝓝 atTop) ↔ ∀ y, ∀ᶠ a in l, Ici y ∈ f a

Proof state:
α : Type u_2
β : Type u_3
inst✝ : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a

Tactic:
simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem HasFiniteIntegral.smul_measure {f : α → β} (h : HasFiniteIntegral f μ) {c : ℝ≥0∞}
    (hc : c ≠ ∞) : HasFiniteIntegral f (c • μ)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : HasFiniteIntegral f μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ HasFiniteIntegral f (c • μ)

Tactic:
simp only [HasFiniteIntegral, lintegral_smul_measure] at *

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
h : ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ c * ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ⊤

Tactic:
exact mul_lt_top hc.lt_top h

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_smul_vadd_smul_vadd_of_nonpos_of_le (x : P) (v : V) {r₁ r₂ : R} (hr₁ : r₁ ≤ 0)
    (hr₂ : r₂ ≤ r₁) : Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : r₁ ≤ 0
hr₂ : r₂ ≤ r₁
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
convert wbtw_smul_vadd_smul_vadd_of_nonneg_of_le x (-v) (Left.nonneg_neg_iff.2 hr₁)
    (neg_le_neg_iff.2 hr₂) using 1 <;>
  rw [neg_smul_neg]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem inner_orthogonalProjection_eq_of_mem_right [HasOrthogonalProjection K] (u : K) (v : E) :
    ⟪orthogonalProjection K v, u⟫ = ⟪v, u⟫ :=
  calc
    ⟪orthogonalProjection K v, u⟫ = ⟪(orthogonalProjection K v : E), u⟫ := K.coe_inner _ _
    _ = ⟪(orthogonalProjection K v : E), u⟫ + ⟪v - orthogonalProjection K v, u⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
u : ↥K
v : E
⊢ ⟪↑((orthogonalProjection K) v), ↑u⟫_𝕜 + ⟪v - ↑((orthogonalProjection K) v), ↑u⟫_𝕜 = ⟪v, ↑u⟫_𝕜

Tactic:
rw [← inner_add_left, add_sub_cancel]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
u : ↥K
v : E
⊢ ⟪↑((orthogonalProjection K) v), ↑u⟫_𝕜 =
    ⟪↑((orthogonalProjection K) v), ↑u⟫_𝕜 + ⟪v - ↑((orthogonalProjection K) v), ↑u⟫_𝕜

Tactic:
rw [orthogonalProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_zero]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem compl_symmDiff_compl : aᶜ ∆ bᶜ = a ∆ b :=
  (sup_comm _ _).trans <| by simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b

Tactic:
simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive sum_pos_iff_of_nonneg]
lemma one_lt_prod_iff_of_one_le (hf : 1 ≤ f) : 1 < ∏ i, f i ↔ 1 < f

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : OrderedCancelCommMonoid M
f : ι → M
hf : 1 ≤ f
⊢ 1 < ∏ i : ι, f i ↔ 1 < f

Tactic:
obtain rfl | hf := hf.eq_or_lt <;> simp [*, one_lt_prod]

Result:
no goals
-- Mathlib/Data/Multiset/Lattice.lean
theorem inf_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).inf = s₁.inf ⊓ s₂.inf

Tactic:
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]

Result:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem ext' (x y : M F) (H : ∀ i : ℕ, x.approx i = y.approx i) : x = y

Proof state:
case mk.mk.e_approx.h
F : PFunctor.{u}
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    { approx := approx✝¹, consistent := consistent✝¹ }.approx i =
      { approx := approx✝, consistent := consistent✝ }.approx i
n : ℕ
⊢ approx✝¹ n = approx✝ n

Tactic:
apply H

Result:
no goals

Proof state:
case mk.mk
F : PFunctor.{u}
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    { approx := approx✝¹, consistent := consistent✝¹ }.approx i =
      { approx := approx✝, consistent := consistent✝ }.approx i
⊢ { approx := approx✝¹, consistent := consistent✝¹ } = { approx := approx✝, consistent := consistent✝ }

Tactic:
congr with n

Result:
case mk.mk.e_approx.h
F : PFunctor.{u}
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    { approx := approx✝¹, consistent := consistent✝¹ }.approx i =
      { approx := approx✝, consistent := consistent✝ }.approx i
n : ℕ
⊢ approx✝¹ n = approx✝ n

Proof state:
case mk
F : PFunctor.{u}
y : F.M
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H : ∀ (i : ℕ), { approx := approx✝, consistent := consistent✝ }.approx i = y.approx i
⊢ { approx := approx✝, consistent := consistent✝ } = y

Tactic:
cases y

Result:
case mk.mk
F : PFunctor.{u}
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    { approx := approx✝¹, consistent := consistent✝¹ }.approx i =
      { approx := approx✝, consistent := consistent✝ }.approx i
⊢ { approx := approx✝¹, consistent := consistent✝¹ } = { approx := approx✝, consistent := consistent✝ }

Proof state:
F : PFunctor.{u}
x y : F.M
H : ∀ (i : ℕ), x.approx i = y.approx i
⊢ x = y

Tactic:
cases x

Result:
case mk
F : PFunctor.{u}
y : F.M
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H : ∀ (i : ℕ), { approx := approx✝, consistent := consistent✝ }.approx i = y.approx i
⊢ { approx := approx✝, consistent := consistent✝ } = y
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_C (r : F) : ((RatFunc.C r : RatFunc F) : F⸨X⸩) = HahnSeries.C r

Proof state:
F : Type u
inst✝ : Field F
r : F
⊢ ↑(C r) = HahnSeries.C r

Tactic:
rw [coe_num_denom, num_C, denom_C, Polynomial.coe_C, Polynomial.coe_one,
  PowerSeries.coe_one, div_one]

Result:
F : Type u
inst✝ : Field F
r : F
⊢ (ofPowerSeries ℤ F) ((PowerSeries.C F) r) = HahnSeries.C r

Proof state:
F : Type u
inst✝ : Field F
r : F
⊢ (ofPowerSeries ℤ F) ((PowerSeries.C F) r) = HahnSeries.C r

Tactic:
simp only [algebraMap_eq_C, ofPowerSeries_C, C_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem equivOfIsometry_trans (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) :
    (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃)

Proof state:
case 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₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
x : CliffordAlgebra Q₁
⊢ ((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃)) x = (equivOfIsometry (e₁₂.trans e₂₃)) x

Tactic:
exact AlgHom.congr_fun (map_comp_map _ _) x

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₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
⊢ (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃)

Tactic:
ext x

Result:
case 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₃
e₁₂ : QuadraticMap.IsometryEquiv Q₁ Q₂
e₂₃ : QuadraticMap.IsometryEquiv Q₂ Q₃
x : CliffordAlgebra Q₁
⊢ ((equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃)) x = (equivOfIsometry (e₁₂.trans e₂₃)) x
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma w₁₃_τ₂ : S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₁₂.τ₂ ≫ S.v₂₃.τ₂ = 0

Tactic:
rw [← comp_τ₂, S.w₁₃, zero_τ₂]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem zero_mem_polar (s : Set E) : (0 : F) ∈ B.polar s := fun _ _ => by
  simp only [map_zero, norm_zero, zero_le_one]

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ‖(B x✝¹) 0‖ ≤ 1

Tactic:
simp only [map_zero, norm_zero, zero_le_one]

Result:
no goals
-- Mathlib/NumberTheory/Padics/MahlerBasis.lean
/-- Bound for iterated forward differences of a continuous function from a compact space to a
nonarchimedean seminormed group. -/
lemma IsUltrametricDist.norm_fwdDiff_iter_apply_le [TopologicalSpace M] [CompactSpace M]
    [AddCommMonoid M] [SeminormedAddCommGroup G] [IsUltrametricDist G]
    (h : M) (f : C(M, G)) (m : M) (n : ℕ) : ‖Δ_[h]^[n] f m‖ ≤ ‖f‖

Proof state:
M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ ‖∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (m + k • h)‖ ≤ ‖f‖

Tactic:
refine norm_sum_le_of_forall_le_of_nonneg (norm_nonneg f) fun i _ ↦ ?_

Result:
M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • f (m + i • h)‖ ≤ ‖f‖

Proof state:
M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • f (m + i • h)‖ ≤ ‖f‖

Tactic:
exact (norm_zsmul_le _ _).trans (f.norm_coe_le_norm _)

Result:
no goals

Proof state:
M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ ‖Δ_[h]^[n] (⇑f) m‖ ≤ ‖f‖

Tactic:
rw [fwdDiff_iter_eq_sum_shift]

Result:
M : Type u_1
G : Type u_2
inst✝⁴ : TopologicalSpace M
inst✝³ : CompactSpace M
inst✝² : AddCommMonoid M
inst✝¹ : SeminormedAddCommGroup G
inst✝ : IsUltrametricDist G
h : M
f : C(M, G)
m : M
n : ℕ
⊢ ‖∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • f (m + k • h)‖ ≤ ‖f‖
-- Mathlib/Topology/MetricSpace/Pseudo/Real.lean
lemma dist_le_of_mem_Icc_01 {x y : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 1) :
    dist x y ≤ 1

Proof state:
x y : ℝ
hx : x ∈ Icc 0 1
hy : y ∈ Icc 0 1
⊢ dist x y ≤ 1

Tactic:
simpa only [sub_zero] using Real.dist_le_of_mem_Icc hx hy

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attachWith_map {l : Vector α n} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
      fun ⟨x, h⟩ => ⟨f x, h⟩

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
P : β → Prop
l : Array α
H : ∀ (b : β), b ∈ map f { toArray := l, size_toArray := ⋯ } → P b
⊢ (map f { toArray := l, size_toArray := ⋯ }).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      ({ toArray := l, size_toArray := ⋯ }.attachWith (P ∘ f) ⋯)

Tactic:
simp [Array.attachWith_map]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β
P : β → Prop
H : ∀ (b : β), b ∈ map f l → P b
⊢ (map f l).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (l.attachWith (P ∘ f) ⋯)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
P : β → Prop
l : Array α
H : ∀ (b : β), b ∈ map f { toArray := l, size_toArray := ⋯ } → P b
⊢ (map f { toArray := l, size_toArray := ⋯ }).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      ({ toArray := l, size_toArray := ⋯ }.attachWith (P ∘ f) ⋯)
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem dvd_gcd_mul_gcd_iff_dvd_mul : x ∣ gcd x n * gcd x m ↔ x ∣ n * m

Proof state:
x n m : ℕ
⊢ x ∣ x.gcd n * x.gcd m ↔ x ∣ n * m

Tactic:
rw [dvd_gcd_mul_iff_dvd_mul, dvd_mul_gcd_iff_dvd_mul]

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem c_of_eq (h : P.toPoly = Q.toPoly) : P.c = Q.c

Proof state:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ P.c = Q.c

Tactic:
rw [← coeff_eq_c, h, coeff_eq_c]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_div_cancel (a b c : G) : a * b / (a / c) = b * c

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * b / (a / c) = b * c

Tactic:
rw [← div_mul, mul_div_cancel_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem le_zero_resolve_left (a c d p x : Int) (h₁ : p ≤ a * x) :
    0 ≤ resolve_left a c d p x

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
⊢ 0 ≤ resolve_left a c d p x

Tactic:
simpa [h₁] using Int.ofNat_nonneg _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_le_size_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List α} :
    m.size ≤ (insertManyIfNewUnit m l).size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
⊢ m.size ≤ (insertManyIfNewUnit m l).size

Tactic:
simp_to_raw using Raw₀.Const.size_le_size_insertManyIfNewUnit_list ⟨m, _⟩

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
lemma coe_one : coe 1 = 1

Proof state:
⊢ ↑1 = 1

Tactic:
simp only [coe, _root_.map_one]

Result:
no goals
-- Mathlib/Algebra/Group/Defs.lean
theorem inv_mul_cancel_left (a b : G) : a⁻¹ * (a * b) = b

Proof state:
G : Type u_1
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = b

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
theorem index_map (f : G →* G') :
    (H.map f).index = (H ⊔ f.ker).index * f.range.index

Proof state:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G →* G'
⊢ (map f H).index = (H ⊔ f.ker).index * f.range.index

Tactic:
rw [← comap_map_eq, index_comap, relindex_mul_index (H.map_le_range f)]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem leftDualIso_id {X Y : C} (p : ExactPairing X Y) : leftDualIso p p = Iso.refl X

Proof state:
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ (leftDualIso p p).hom = (Iso.refl X).hom

Tactic:
simp only [leftDualIso, Iso.refl_hom, @leftAdjointMate_id _ _ _ _ ⟨X⟩]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ leftDualIso p p = Iso.refl X

Tactic:
ext

Result:
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ (leftDualIso p p).hom = (Iso.refl X).hom