harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Basic.lean
theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
  ⟨fun h => by cases h; assumption, LiftRel.inr⟩

Proof state:
case inr
α✝ : Type u_1
γ✝ : Type u_2
r : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
s : β✝ → δ✝ → Prop
b : β✝
d : δ✝
a✝ : s b d
⊢ s b d

Tactic:
assumption

Result:
no goals

Proof state:
α✝ : Type u_1
γ✝ : Type u_2
r : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
s : β✝ → δ✝ → Prop
b : β✝
d : δ✝
h : LiftRel r s (inr b) (inr d)
⊢ s b d

Tactic:
cases h

Result:
case inr
α✝ : Type u_1
γ✝ : Type u_2
r : α✝ → γ✝ → Prop
β✝ : Type u_3
δ✝ : Type u_4
s : β✝ → δ✝ → Prop
b : β✝
d : δ✝
a✝ : s b d
⊢ s b d
-- Mathlib/Tactic/CategoryTheory/BicategoricalComp.lean
theorem bicategoricalComp_refl {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) : η ⊗≫ θ = η ≫ θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ⊗≫ θ = η ≫ θ

Tactic:
dsimp [bicategoricalComp]

Result:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ η ≫ 𝟙 g ≫ θ = η ≫ θ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Units.lean
theorem Fintype.card_units [GroupWithZero α] [Fintype α] [DecidableEq α] :
    Fintype.card αˣ = Fintype.card α - 1

Proof state:
α : Type u_1
inst✝² : GroupWithZero α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card αˣ = card α - 1

Tactic:
rw [← Nat.card_eq_fintype_card, Nat.card_units, Nat.card_eq_fintype_card]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRight_nil {f g : C} (α : f ≅ g) (h : C) :
    (whiskerRightIso α h).hom = (whiskerRightIso α h).hom

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g : C
α : f ≅ g
h : C
⊢ (whiskerRightIso α h).hom = (whiskerRightIso α h).hom

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/NumberField/House.lean
theorem house_intCast (x : ℤ) : house (x : K) = |x|

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : ℤ
⊢ house ↑x = ↑|x|

Tactic:
simp only [house, map_intCast, Pi.intCast_def, pi_norm_const, Complex.norm_intCast, Int.cast_abs]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/ParallelComp.lean
/-- For a deterministic kernel, copying then applying the kernel to the two copies is the same
as first applying the kernel then copying. -/
lemma deterministic_comp_copy {f : α → β} (hf : Measurable f) :
    (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₖ Kernel.copy α
      = Kernel.copy β ∘ₖ Kernel.deterministic f hf

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf

Tactic:
simp_rw [Kernel.parallelComp_comp_copy, Kernel.deterministic_prod_deterministic,
  Kernel.copy, Kernel.deterministic_comp_deterministic, Function.comp_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_mul_conjTranspose_self [Fintype n] (A : Matrix m n α) :
    (A * Aᴴ).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝² : NonUnitalSemiring α
inst✝¹ : StarRing α
inst✝ : Fintype n
A : Matrix m n α
⊢ (A * Aᴴ).IsHermitian

Tactic:
rw [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_zero' : √x = 0 ↔ x ≤ 0

Proof state:
x : ℝ
⊢ √x = 0 ↔ x ≤ 0

Tactic:
rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_alterKey {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} :
    (alterKey k f l).isEmpty = ((l.isEmpty || (l.length == 1 && containsKey k l)) &&
      (f (getValue? k l)).isNone)

Proof state:
α : Type u
inst✝ : BEq α
β : Type v
k : α
f : Option β → Option β
l : List ((_ : α) × β)
⊢ (alterKey k f l).isEmpty = ((l.isEmpty || l.length == 1 && containsKey k l) && (f (getValue? k l)).isNone)

Tactic:
rw [isEmpty_alterKey_eq_isEmpty_eraseKey, isEmpty_eraseKey]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem continuous_mul' (g : GroupTopology α) :
    haveI := g.toTopologicalSpace
    Continuous fun p : α × α => p.1 * p.2

Proof state:
α : Type u
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous fun p => p.1 * p.2

Tactic:
haveI := g.toIsTopologicalGroup

Result:
α : Type u
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous fun p => p.1 * p.2

Proof state:
α : Type u
inst✝ : Group α
g : GroupTopology α
this✝ : TopologicalSpace α := g.toTopologicalSpace
this : IsTopologicalGroup α
⊢ Continuous fun p => p.1 * p.2

Tactic:
exact continuous_mul

Result:
no goals

Proof state:
α : Type u
inst✝ : Group α
g : GroupTopology α
⊢ Continuous fun p => p.1 * p.2

Tactic:
letI := g.toTopologicalSpace

Result:
α : Type u
inst✝ : Group α
g : GroupTopology α
this : TopologicalSpace α := g.toTopologicalSpace
⊢ Continuous fun p => p.1 * p.2
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem rightUnitor_inv_naturality {X X' : C} (f : X ⟶ X') :
    f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ f ▷ _

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' : C
f : X ⟶ X'
⊢ f ≫ (ρ_ X').inv = (ρ_ X).inv ≫ f ▷ 𝟙_ C

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem tendsto_add_atTop_iff_nat {f : ℕ → α} {l : Filter α} (k : ℕ) :
    Tendsto (fun n => f (n + k)) atTop l ↔ Tendsto f atTop l :=
  show Tendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l by
    rw [← tendsto_map'_iff, map_add_atTop_eq_nat]

Proof state:
α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto (f ∘ fun n => n + k) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← tendsto_map'_iff, map_add_atTop_eq_nat]

Result:
no goals
-- Mathlib/Algebra/Homology/DifferentialObject.lean
theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}
    (h : x = y) : X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h

Proof state:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x y : β
h : x = y
⊢ X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h

Tactic:
cases h

Result:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem initial.hom_ext [HasInitial C] {P : C} (f g : ⊥_ C ⟶ P) : f = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P : C
f g : ⊥_ C ⟶ P
⊢ f = g

Tactic:
ext ⟨⟨⟩⟩

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
theorem sdiff_subset_sdiff_iff_subset {r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) :
    r \ s ⊆ r \ t ↔ t ⊆ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t r : Finset α
hs : s ⊆ r
ht : t ⊆ r
⊢ r \ s ⊆ r \ t ↔ t ⊆ s

Tactic:
simpa only [← le_eq_subset] using sdiff_le_sdiff_iff_le hs ht

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem mem_infPrepartition_comm :
    J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition

Proof state:
ι : Type u_1
I J : Box ι
π₁ π₂ : TaggedPrepartition I
⊢ J ∈ π₁.infPrepartition π₂.toPrepartition ↔ J ∈ π₂.infPrepartition π₁.toPrepartition

Tactic:
simp only [← mem_toPrepartition, infPrepartition_toPrepartition, inf_comm]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_inter_Ioo_of_left_lt (h : b₁ < b₂) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁ :=
  ext fun x => by
    simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₁ < b₂
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioc (a₁ ⊔ a₂) b₁

Tactic:
simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem get_iterate (f : α → α) (a : α) (n : ℕ) (i : Fin (iterate f a n).length) :
    get (iterate f a n) i = f^[↑i] a

Proof state:
α : Type u_1
f : α → α
a : α
n : ℕ
i : Fin (iterate f a n).length
⊢ (iterate f a n).get i = f^[↑i] a

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_equation (hf : Function.Injective f) :
    (W'.map f).toAffine.Equation (f x) (f y) ↔ W'.Equation x y

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x y : R
hf : Function.Injective ⇑f
⊢ (map W' f).toAffine.Equation (f x) (f y) ↔ W'.Equation x y

Tactic:
simp only [Equation, map_polynomial, map_mapRingHom_evalEval, map_eq_zero_iff f hf]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_le_iff' : a \ b ≤ c ↔ a ≤ c ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ≤ c ↔ a ≤ c ⊔ b

Tactic:
rw [sdiff_le_iff, sup_comm]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_biUnion (πi : ∀ J : Box ι, Prepartition J) :
    (π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
⊢ (π.biUnion πi).iUnion = ⋃ J ∈ π, (πi J).iUnion

Tactic:
simp [Prepartition.iUnion]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_c₄ : (W.map φ).c₄ = φ W.c₄

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).c₄ = φ W.c₄

Tactic:
simp only [c₄, map_b₂, map_b₄]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.b₂ ^ 2 - 24 * φ W.b₄ = φ (W.b₂ ^ 2 - 24 * W.b₄)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.b₂ ^ 2 - 24 * φ W.b₄ = φ (W.b₂ ^ 2 - 24 * W.b₄)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_dvd {i j k : ℤ} : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k

Proof state:
i j k : ℤ
⊢ i ∣ k → j ∣ k → ↑(i.lcm j) ∣ k

Tactic:
rw [Int.lcm]

Result:
i j k : ℤ
⊢ i ∣ k → j ∣ k → ↑(i.natAbs.lcm j.natAbs) ∣ k

Proof state:
i j k : ℤ
⊢ i ∣ k → j ∣ k → ↑(i.natAbs.lcm j.natAbs) ∣ k

Tactic:
intro hi hj

Result:
i j k : ℤ
hi : i ∣ k
hj : j ∣ k
⊢ ↑(i.natAbs.lcm j.natAbs) ∣ k

Proof state:
i j k : ℤ
hi : i ∣ k
hj : j ∣ k
⊢ ↑(i.natAbs.lcm j.natAbs) ∣ k

Tactic:
exact natCast_dvd.mpr (Nat.lcm_dvd (natAbs_dvd_natAbs.mpr hi) (natAbs_dvd_natAbs.mpr hj))

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[reassoc (attr := simp)]
lemma LeftHomologyData.liftCycles_comp_cyclesIso_hom :
    S.liftCycles k hk ≫ h.cyclesIso.hom = h.liftK k hk

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝ : S.HasLeftHomology
⊢ S.liftCycles k hk ≫ h.cyclesIso.hom = h.liftK k hk

Tactic:
simp only [← cancel_mono h.i, assoc, LeftHomologyData.cyclesIso_hom_comp_i,
  liftCycles_i, LeftHomologyData.liftK_i]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `lt_inv_mul_iff₀` for a version with multiplication on the other side. -/
lemma lt_inv_mul_iff₀' (hc : 0 < c) : a < c⁻¹ * b ↔ a * c < b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
⊢ a < c⁻¹ * b ↔ a * c < b

Tactic:
rw [lt_inv_mul_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem neg_iff : z < 0 ↔ re z < 0 ∧ im z = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ re z < 0 ∧ im z = 0

Tactic:
simpa only [map_zero] using lt_iff_re_im (z := z) (w := 0)

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem isRegular_star_iff [Mul R] [StarMul R] {x : R} :
    IsRegular (star x) ↔ IsRegular x

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsRegular (star x) ↔ IsRegular x

Tactic:
rw [isRegular_iff, isRegular_iff, isRightRegular_star_iff, isLeftRegular_star_iff, and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem le_iff_lt_or_eq [DecidableEq α] [LT α] [DecidableLT α]
    [Std.Irrefl (· < · : α → α → Prop)]
    [Std.Antisymm (¬ · < · : α → α → Prop)]
    [Std.Total (¬ · < · : α → α → Prop)]
    {l₁ l₂ : Vector α n} : l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

Proof state:
α : Type u_1
n : Nat
inst✝⁵ : DecidableEq α
inst✝⁴ : LT α
inst✝³ : DecidableLT α
inst✝² : Std.Irrefl fun x1 x2 => x1 < x2
inst✝¹ : Std.Antisymm fun x1 x2 => ¬x1 < x2
inst✝ : Std.Total fun x1 x2 => ¬x1 < x2
l₁ l₂ : Vector α n
⊢ l₁ ≤ l₂ ↔ l₁ < l₂ ∨ l₁ = l₂

Tactic:
simpa using Array.le_iff_lt_or_eq (l₁ := l₁.toArray) (l₂ := l₂.toArray)

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@[simp]
lemma bot_lt_add [LT α] : ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Proof state:
α : Type u
inst✝¹ : Add α
x y : WithBot α
inst✝ : LT α
⊢ ⊥ < x + y ↔ ⊥ < x ∧ ⊥ < y

Tactic:
simp_rw [WithBot.bot_lt_iff_ne_bot, add_ne_bot]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem exists_wellOrder : ∃ (_ : LinearOrder α), WellFoundedLT α

Proof state:
α : Type u
⊢ ∃ x, WellFoundedLT α

Tactic:
classical
exact ⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩

Result:
no goals

Proof state:
α : Type u
⊢ ∃ x, WellFoundedLT α

Tactic:
exact ⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem addInequality_sat (w : c + Coeffs.dot x y ≥ 0) :
    Constraint.sat' { lowerBound := some (-c), upperBound := none } x y

Proof state:
c : Int
x y : Coeffs
w : c + x.dot y ≥ 0
⊢ -c ≤ x.dot y

Tactic:
rw [← Int.zero_sub c]

Result:
c : Int
x y : Coeffs
w : c + x.dot y ≥ 0
⊢ 0 - c ≤ x.dot y

Proof state:
c : Int
x y : Coeffs
w : c + x.dot y ≥ 0
⊢ { lowerBound := some (-c), upperBound := none }.sat' x y = true

Tactic:
simp [Constraint.sat', Constraint.sat]

Result:
c : Int
x y : Coeffs
w : c + x.dot y ≥ 0
⊢ -c ≤ x.dot y

Proof state:
c : Int
x y : Coeffs
w : c + x.dot y ≥ 0
⊢ 0 - c ≤ x.dot y

Tactic:
exact Int.sub_left_le_of_le_add w

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_node3R (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
    dual (node3R l x m y r) = node3L (dual r) y (dual m) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3R x m y r).dual = r.dual.node3L y m.dual x l.dual

Tactic:
simp [node3L, node3R, dual_node', add_comm]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Ico : (some : α → WithBot α) ⁻¹' Ico a b = Ico a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b

Tactic:
simp [← Ici_inter_Iio]

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_congr (_ : a = a') (_ : b = b') (_ : a' * b' = c) : (a * b : R) = c

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a a' b b' c : R
x✝² : a = a'
x✝¹ : b = b'
x✝ : a' * b' = c
⊢ a * b = c

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a' b' : R
⊢ a' * b' = a' * b'
-- Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
theorem toMatrix_row_sum_one [Fintype ι] (q : ι' → P) (i : ι') : ∑ j, b.toMatrix q i j = 1

Proof state:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst✝⁴ : AddCommGroup V
inst✝³ : AffineSpace V P
inst✝² : Ring k
inst✝¹ : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst✝ : Fintype ι
q : ι' → P
i : ι'
⊢ ∑ j : ι, b.toMatrix q i j = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_le_iff_left : a - b ≤ c ↔ a ≤ b + c

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
rw [tsub_le_iff_right, add_comm]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem mul_eq_left₀ (ha : a ≠ 0) : a * b = a ↔ b = 1

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
a b : M₀
ha : a ≠ 0
⊢ a * b = a ↔ b = 1

Tactic:
rw [Iff.comm, ← mul_right_inj' ha, mul_one]

Result:
no goals
-- Mathlib/Deprecated/Cardinal/PartENat.lean
theorem toPartENat_lift (c : Cardinal.{v}) : toPartENat (lift.{u, v} c) = toPartENat c

Proof state:
c : Cardinal.{v}
⊢ toPartENat (lift.{u, v} c) = toPartENat c

Tactic:
simp only [← partENatOfENat_toENat, toENat_lift]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioo_subset_Iio_self : Ioo a b ⊆ Iio b

Proof state:
α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Iio b

Tactic:
simpa [← coe_subset] using Set.Ioo_subset_Iio_self

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Normed.lean
theorem tsupport_normed_eq : tsupport (f.normed μ) = Metric.closedBall c f.rOut

Proof state:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ tsupport (f.normed μ) = closedBall c f.rOut

Tactic:
rw [tsupport, f.support_normed_eq, closure_ball _ f.rOut_pos.ne']

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Iic (hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) :
    (Iic a).map (Embedding.subtype p) = (Iic a : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Iic a) = Iic ↑a

Tactic:
rw [subtype_Iic_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Iic ↑a)) = Iic ↑a

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Iic ↑a)) = Iic ↑a

Tactic:
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iic.1 hx) a.prop

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean
theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : Scheme)
    {U : X.Opens} (hU : IsAffineOpen U) (x f : Γ(X, U))
    (H : x |_ (X.basicOpen f) = 0) :
    ∃ n : ℕ, f ^ n * x = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
obtain ⟨n, e⟩ :=
  @IsLocalization.Away.exists_of_eq _ _ _ _ _ _ (hU.isLocalization_basicOpen f) _ _ H

Result:
case intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ ∃ n, f ^ n * x = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op).hom] at H

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
⊢ ∃ n, f ^ n * x = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ f ^ n * x = 0

Tactic:
simpa [mul_comm x] using e

Result:
no goals

Proof state:
case intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) 0
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
exact ⟨n, by simpa [mul_comm x] using e⟩

Result:
no goals
-- Mathlib/CategoryTheory/Products/Basic.lean
/-- Any morphism in a product factors as a morphsim whose right component is an identity
followed by a morphism whose left component is an identity. -/
@[reassoc]
lemma fac' {x y : C × D} (f : x ⟶ y) :
    f = ((f.1, 𝟙 x.2) : _ ⟶ ⟨y.1, x.2⟩) ≫ (𝟙 y.1, f.2)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C × D
f : x ⟶ y
⊢ f = (f.1, 𝟙 x.2) ≫ (𝟙 y.1, f.2)

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma uniq_var (g : relations.G) : uniq h h' (solution.var g) = solution'.var g

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ (h.uniq h') (solution.var g) = solution'.var g

Tactic:
simp [uniq]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.nat_odd_mul_antiperiodic [Semiring α] [InvolutiveNeg β] (h : Antiperiodic f c)
    (n : ℕ) : Antiperiodic f (n * (2 * c) + c) := fun x => by
  rw [← add_assoc, h, h.nat_even_mul_periodic]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : Semiring α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℕ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
rw [← add_assoc, h, h.nat_even_mul_periodic]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_eval_sub {R} [CommRing R] (r : R) (f : R[X]) (s : R) :
    (taylor r f).eval (s - r) = f.eval s

Proof state:
R : Type u_2
inst✝ : CommRing R
r : R
f : R[X]
s : R
⊢ eval (s - r) ((taylor r) f) = eval s f

Tactic:
rw [taylor_eval, sub_add_cancel]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma eulerMascheroniSeq'_one : eulerMascheroniSeq' 1 = 1

Proof state:
⊢ eulerMascheroniSeq' 1 = 1

Tactic:
simp [eulerMascheroniSeq']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem dropSuffix?_nil [BEq α] {s : List α} : dropSuffix? s [] = some s

Proof state:
α : Type u_1
inst✝ : BEq α
s : List α
⊢ s.dropSuffix? [] = some s

Tactic:
simp [dropSuffix?_eq_some_iff]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_self [Nontrivial α] {p : Associates α}
    (hp : Irreducible p) : p.count p.factors = 1

Proof state:
α : Type u_1
inst✝⁴ : CancelCommMonoidWithZero α
inst✝³ : UniqueFactorizationMonoid α
inst✝² : DecidableEq (Associates α)
inst✝¹ : (p : Associates α) → Decidable (Irreducible p)
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p.count p.factors = 1

Tactic:
simp [factors_self hp, Associates.count_some hp]

Result:
no goals