harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_eq_comm {a b : Int} : -a = b ↔ -b = a

Proof state:
a b : Int
⊢ -a = b ↔ -b = a

Tactic:
rw [eq_comm, Int.eq_neg_comm, eq_comm]

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
lemma Algebra.IsPushout.equiv_symm_algebraMap_left [Algebra.IsPushout R S R' S'] (a : S) :
    (equiv R S R' S').symm (algebraMap S S' a) = a ⊗ₜ 1

Proof state:
R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : S
⊢ (equiv R S R' S').symm ((algebraMap S S') a) = a ⊗ₜ[R] 1

Tactic:
rw [(equiv R S R' S').symm_apply_eq, equiv_tmul, map_one, mul_one]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Field.lean
@[simp, norm_cast]
lemma cast_div_charZero (hnm : n ∣ m) : (↑(m / n) : K) = m / n

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hnm : n ∣ m
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
obtain rfl | hn := eq_or_ne n 0 <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp, reassoc]
lemma right_unitality (X : C) :
    (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ δ F X (𝟙_ C) ≫ F.obj X ◁ η F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
⊢ (ρ_ (F.obj X)).inv = F.map (ρ_ X).inv ≫ δ F X (𝟙_ C) ≫ F.obj X ◁ η F

Tactic:
apply oplax_right_unitality'

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem mul_den (q₁ q₂ : ℚ) :
    (q₁ * q₂).den =
      q₁.den * q₂.den / Nat.gcd (q₁.num * q₂.num).natAbs (q₁.den * q₂.den)

Proof state:
q₁ q₂ : ℚ
⊢ (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)

Tactic:
rw [mul_def, normalize_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
lemma volume_euclideanSpace_eq_dirac [IsEmpty ι] :
    (volume : Measure (EuclideanSpace ℝ ι)) = Measure.dirac 0

Proof state:
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : IsEmpty ι
⊢ volume = dirac 0

Tactic:
rw [← ((EuclideanSpace.volume_preserving_measurableEquiv ι).symm).map_eq,
  volume_pi_eq_dirac 0, map_dirac (MeasurableEquiv.measurable _),
  EuclideanSpace.coe_measurableEquiv_symm, WithLp.equiv_symm_zero]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
theorem inr_star [AddMonoid R] [StarAddMonoid R] [Star A] (a : A) :
    ↑(star a) = star (a : Unitization R A) :=
  ext (by simp only [fst_star, star_zero, fst_inr]) rfl

Proof state:
R : Type u_1
A : Type u_2
inst✝² : AddMonoid R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ (↑(star a)).fst = (star ↑a).fst

Tactic:
simp only [fst_star, star_zero, fst_inr]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigOWith.sub (h₁ : IsBigOWith c₁ l f₁ g) (h₂ : IsBigOWith c₂ l f₂ g) :
    IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x => f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b)

Proof state:
a b : Prop
⊢ (a ∨ b ↔ b) ↔ a → b

Tactic:
rw [or_comm, or_iff_left_iff_imp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem back?_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).back? = xs.attach.back?.map fun ⟨a, m⟩ => f a (H a m)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
P : α → Prop
f : (a : α) → P a → β
xs : Vector α n
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.back?

Tactic:
cases xs

Result:
case mk
α : Type u_1
β : Type u_2
n : Nat
P : α → Prop
f : (a : α) → P a → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ (pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.back?

Proof state:
case mk
α : Type u_1
β : Type u_2
n : Nat
P : α → Prop
f : (a : α) → P a → β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → P a
⊢ (pmap f { toArray := toArray✝, size_toArray := size_toArray✝ } H).back? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.back?

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_sub_one (a : α) : round (a - 1) = round a - 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a - 1) = round a - 1

Tactic:
rw [← round_sub_int a 1, cast_one]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
lemma extend_d_eq {i' j' : ι'} {i j : ι} (hi : e.f i = i') (hj : e.f j = j') :
    (K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫
      (K.extendXIso e hj).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i j : ι
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv

Tactic:
apply extend.d_eq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_attach (l : List α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
    pmap f l.attach H =
      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩)

Proof state:
α : Type ?u.41668
β : Type ?u.41712
l : List α
p : { x // x ∈ l } → Prop
f : (a : { x // x ∈ l }) → p a → β
H : ∀ (a : { x // x ∈ l }), a ∈ l.attach → p a
a : α
h : a ∈ l
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
p : { x // x ∈ l } → Prop
f : (a : { x // x ∈ l }) → p a → β
H : ∀ (a : { x // x ∈ l }), a ∈ l.attach → p a
⊢ pmap f l.attach H = pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯

Tactic:
apply ext_getElem <;> simp

Result:
no goals
-- Mathlib/Data/Subtype.lean
lemma heq_iff_coe_heq {α β : Sort _} {p : α → Prop} {q : β → Prop} {a : {x // p x}}
    {b : {y // q y}} (h : α = β) (h' : HEq p q) : HEq a b ↔ HEq (a : α) (b : β)

Proof state:
α : Sort u_4
p : α → Prop
a b : { y // p y }
⊢ HEq a b ↔ HEq ↑a ↑b

Tactic:
rw [heq_iff_eq, heq_iff_eq, Subtype.ext_iff]

Result:
no goals

Proof state:
α β : Sort u_4
p : α → Prop
q : β → Prop
a : { x // p x }
b : { y // q y }
h : α = β
h' : HEq p q
⊢ HEq a b ↔ HEq ↑a ↑b

Tactic:
subst h

Result:
α : Sort u_4
p : α → Prop
a : { x // p x }
q : α → Prop
b : { y // q y }
h' : HEq p q
⊢ HEq a b ↔ HEq ↑a ↑b

Proof state:
α : Sort u_4
p : α → Prop
a : { x // p x }
q : α → Prop
b : { y // q y }
h' : HEq p q
⊢ HEq a b ↔ HEq ↑a ↑b

Tactic:
subst h'

Result:
α : Sort u_4
p : α → Prop
a b : { y // p y }
⊢ HEq a b ↔ HEq ↑a ↑b
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem weightedSMul_smul [NormedField 𝕜] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜)
    (s : Set α) (x : F) : weightedSMul μ s (c • x) = c • weightedSMul μ s x

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
c : 𝕜
s : Set α
x : F
⊢ (weightedSMul μ s) (c • x) = c • (weightedSMul μ s) x

Tactic:
simp_rw [weightedSMul_apply, smul_comm]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem expand_card {p : ℕ} [Fact p.Prime] (f : Polynomial (ZMod p)) :
    expand (ZMod p) p f = f ^ p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ (expand (ZMod p) p) f = f ^ p

Tactic:
have h := FiniteField.expand_card f

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : (expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ (expand (ZMod p) p) f = f ^ p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : (expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ (expand (ZMod p) p) f = f ^ p

Tactic:
rwa [ZMod.card p] at h

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem hasStrictFDerivAt_sub_const_iff (c : F) :
    HasStrictFDerivAt (f · - c) f' x ↔ HasStrictFDerivAt f f' x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun x => f x - c) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
simp only [sub_eq_add_neg, hasStrictFDerivAt_add_const_iff]

Result:
no goals
-- Mathlib/Data/Fintype/Sum.lean
theorem Fintype.card_subtype_or (p q : α → Prop) [Fintype { x // p x }] [Fintype { x // q x }]
    [Fintype { x // p x ∨ q x }] :
    Fintype.card { x // p x ∨ q x } ≤ Fintype.card { x // p x } + Fintype.card { x // q x }

Proof state:
case h.e'_4
α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })

Tactic:
rw [Fintype.card_sum]

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }

Tactic:
classical
  convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
  rw [Fintype.card_sum]

Result:
no goals

Proof state:
α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }

Tactic:
convert Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)

Result:
case h.e'_4
α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x } + card { x // q x } = card ({ x // p x } ⊕ { x // q x })
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
@[simp] lemma neg_apply {f : E →WOT[𝕜] F} (x : E) : (-f) x = -(f x)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f : E →WOT[𝕜] F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (-f))).toFun x =
    -(↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f : E →WOT[𝕜] F
x : E
⊢ (-f) x = -f x

Tactic:
simp only [DFunLike.coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
f : E →WOT[𝕜] F
x : E
⊢ (↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm (-f))).toFun x =
    -(↑(EquivLike.coe (ContinuousLinearMap.toWOT 𝕜 E F).symm f)).toFun x
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem isCoprime_iff_gcd {I J : Ideal A} : IsCoprime I J ↔ gcd I J = 1

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
⊢ IsCoprime I J ↔ gcd I J = 1

Tactic:
rw [Ideal.isCoprime_iff_codisjoint, codisjoint_iff, one_eq_top, gcd_eq_sup]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range_eq_empty_iff {n : Nat} : range n = #[] ↔ n = 0

Proof state:
n : Nat
⊢ range n = #[] ↔ n = 0

Tactic:
rw [← size_eq_zero, size_range]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
    l.toArray.foldrM f init = l.foldrM f init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ Array.foldrM f init l.toArray = foldrM f init l

Tactic:
rw [foldrM_eq_reverse_foldlM_toList]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ List.foldlM (fun x y => f y x) init l.toArray.toList.reverse = foldrM f init l

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
l : List α
⊢ List.foldlM (fun x y => f y x) init l.toArray.toList.reverse = foldrM f init l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
    (h : stop = l.toArray.size) :
    l.toArray.foldl f init 0 stop = l.foldl f init

Proof state:
β : Type u_1
α : Type u_2
stop : Nat
f : β → α → β
init : β
l : List α
h : stop = l.toArray.size
⊢ Array.foldl f init l.toArray 0 stop = foldl f init l

Tactic:
subst h

Result:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
l : List α
⊢ Array.foldl f init l.toArray = foldl f init l

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
init : β
l : List α
⊢ Array.foldl f init l.toArray = foldl f init l

Tactic:
rw [foldl_toList]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
    j.succ.castSucc = (j.castSucc).succ

Proof state:
n : Nat
j : Fin n
⊢ j.succ.castSucc = j.castSucc.succ

Tactic:
simp [Fin.ext_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
lemma charmatrix_map (M : Matrix n n R) (f : R →+* S) :
    charmatrix (M.map f) = (charmatrix M).map (Polynomial.map f)

Proof state:
case a.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n✝ : ℕ
⊢ ((M.map ⇑f).charmatrix i j).coeff n✝ = (M.charmatrix.map (Polynomial.map f) i j).coeff n✝

Tactic:
by_cases h : i = j <;> simp [h, charmatrix, diagonal]

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
⊢ (M.map ⇑f).charmatrix = M.charmatrix.map (Polynomial.map f)

Tactic:
ext i j

Result:
case a.a
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
n : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
f : R →+* S
i j : n
n✝ : ℕ
⊢ ((M.map ⇑f).charmatrix i j).coeff n✝ = (M.charmatrix.map (Polynomial.map f) i j).coeff n✝
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_apply_pi {ι : Type*} (f : ι → R → R) (a : A) (ha

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (∀ (i : ι), ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ (i : ι), f i 0 = 0) _auto✝
⊢ (fun i => cfcₙ (f i) a) = fun i =>
    (cfcₙHom ha) { toFun := (σₙ R a).restrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
ext i

Result:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (∀ (i : ι), ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ (i : ι), f i 0 = 0) _auto✝
i : ι
⊢ cfcₙ (f i) a = (cfcₙHom ha) { toFun := (σₙ R a).restrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Proof state:
case h
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
ι : Type u_3
f : ι → R → R
a : A
ha : autoParam (p a) _auto✝
hf : autoParam (∀ (i : ι), ContinuousOn (f i) (σₙ R a)) _auto✝
hf0 : autoParam (∀ (i : ι), f i 0 = 0) _auto✝
i : ι
⊢ cfcₙ (f i) a = (cfcₙHom ha) { toFun := (σₙ R a).restrict (f i), continuous_toFun := ⋯, map_zero' := ⋯ }

Tactic:
simp only [cfcₙ_apply (f i) a (hf i) (hf0 i)]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addZ_of_Z_eq_zero_left {P Q : Fin 3 → R} (hPz : P z = 0) : addZ P Q = P x * Q z * Q z

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ addZ P Q = P x * Q z * Q z

Tactic:
rw [addZ, hPz]

Result:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * 0 ^ 2 = P x * Q z * Q z

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * 0 ^ 2 = P x * Q z * Q z

Tactic:
ring1

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma induce_union_connected {H : G.Subgraph} {s t : Set V}
    (sconn : (H.induce s).Connected) (tconn : (H.induce t).Connected)
    (sintert : (s ⊓ t).Nonempty) :
    (H.induce (s ∪ t)).Connected

Proof state:
case refine_2
V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Connected
tconn : (H.induce t).Connected
sintert : (s ⊓ t).Nonempty
⊢ (H.induce s ⊔ H.induce t).verts = (H.induce (s ∪ t)).verts

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Connected
tconn : (H.induce t).Connected
sintert : (s ⊓ t).Nonempty
⊢ H.induce s ⊔ H.induce t ≤ H.induce (s ∪ t)

Tactic:
apply le_induce_union

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Connected
tconn : (H.induce t).Connected
sintert : (s ⊓ t).Nonempty
⊢ (H.induce (s ∪ t)).Connected

Tactic:
refine (sconn.sup tconn sintert).mono ?_ ?_

Result:
case refine_1
V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Connected
tconn : (H.induce t).Connected
sintert : (s ⊓ t).Nonempty
⊢ H.induce s ⊔ H.induce t ≤ H.induce (s ∪ t)

case refine_2
V : Type u
G : SimpleGraph V
H : G.Subgraph
s t : Set V
sconn : (H.induce s).Connected
tconn : (H.induce t).Connected
sintert : (s ⊓ t).Nonempty
⊢ (H.induce s ⊔ H.induce t).verts = (H.induce (s ∪ t)).verts
-- Mathlib/Data/NNReal/Defs.lean
theorem toNNReal_lt_iff_lt_coe {r : ℝ} {p : ℝ≥0} (ha : 0 ≤ r) : Real.toNNReal r < p ↔ r < ↑p

Proof state:
r : ℝ
p : ℝ≥0
ha : 0 ≤ r
⊢ r.toNNReal < p ↔ r < ↑p

Tactic:
rw [← NNReal.coe_lt_coe, Real.coe_toNNReal r ha]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem mapRange_sub [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : G → H} {hf : f 0 = 0}
    (hf' : ∀ x y, f (x - y) = f x - f y) (v₁ v₂ : α →₀ G) :
    mapRange f hf (v₁ - v₂) = mapRange f hf v₁ - mapRange f hf v₂ :=
  ext fun _ => by simp only [hf', sub_apply, mapRange_apply]

Proof state:
α : Type u_1
G : Type u_9
H : Type u_10
inst✝¹ : SubNegZeroMonoid G
inst✝ : SubNegZeroMonoid H
f : G → H
hf : f 0 = 0
hf' : ∀ (x y : G), f (x - y) = f x - f y
v₁ v₂ : α →₀ G
x✝ : α
⊢ (mapRange f hf (v₁ - v₂)) x✝ = (mapRange f hf v₁ - mapRange f hf v₂) x✝

Tactic:
simp only [hf', sub_apply, mapRange_apply]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_range_le_centralizer :
    (kerParam g).range ≤ Subgroup.centralizer {g}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ map (centralizer {g}).subtype (toPermHom g).ker ≤ centralizer {g}

Tactic:
exact map_subtype_le (toPermHom g).ker

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ (kerParam g).range ≤ centralizer {g}

Tactic:
rw [kerParam_range_eq]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ map (centralizer {g}).subtype (toPermHom g).ker ≤ centralizer {g}
-- Mathlib/Data/Set/Prod.lean
theorem union_prod : (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
simp [or_and_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
⊢ (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma isStandardSmooth_holdsForLocalizationAway :
    HoldsForLocalizationAway IsStandardSmooth.{0, 0}

Proof state:
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => IsStandardSmooth

Tactic:
introv R h

Result:
R S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).IsStandardSmooth

Proof state:
R S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).IsStandardSmooth

Tactic:
exact (IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r).isStandardSmooth

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β} :
    (Const.modify m k f).getKey! k' =
      if k == k' then
        if m.contains k then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
inst✝ : Inhabited α
k k' : α
f : β → β
⊢ (modify m k f).getKey! k' = if (k == k') = true then if m.contains k = true then k else default else m.getKey! k'

Tactic:
simp_to_model [Const.modify] using List.Const.getKey!_modifyKey

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedSup_union_right (hs : a ∉ lowerClosure s) (ht : a ∈ lowerClosure t) :
    truncatedSup (s ∪ t) a = truncatedSup t a

Proof state:
α : Type u_1
inst✝³ : SemilatticeSup α
s t : Finset α
a : α
inst✝² : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
hs : a ∉ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ (s ∪ t).truncatedSup a = t.truncatedSup a

Tactic:
rw [union_comm, truncatedSup_union_left ht hs]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma one_le_sqrt : 1 ≤ sqrt x ↔ 1 ≤ x

Proof state:
x : ℝ≥0
⊢ 1 ≤ sqrt x ↔ 1 ≤ x

Tactic:
rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]

Result:
no goals