harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Iso.lean
theorem refl_trans (α : X ≅ Y) : Iso.refl X ≪≫ α = α

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom

Tactic:
apply Category.id_comp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ refl X ≪≫ α = α

Tactic:
ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_replicate {n : Nat} {a : α} {l : List α} :
    l ~ replicate n a ↔ l = replicate n a

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
p : l ~ replicate n a
⊢ l.length = n ∧ ∀ (b : α), b ∈ l → b = a

Tactic:
exact ⟨p.length_eq.trans <| length_replicate .., fun _b m => eq_of_mem_replicate <| p.subset m⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ l ~ replicate n a ↔ l = replicate n a

Tactic:
refine ⟨fun p => eq_replicate_iff.2 ?_, fun h => h ▸ .rfl⟩

Result:
α : Type u_1
n : Nat
a : α
l : List α
p : l ~ replicate n a
⊢ l.length = n ∧ ∀ (b : α), b ∈ l → b = a
-- Mathlib/CategoryTheory/Category/RelCat.lean
theorem rel_id_apply₂ (X : RelCat) (x y : X) : (𝟙 X) x y ↔ x = y

Proof state:
X : RelCat
x y : X
⊢ 𝟙 X x y ↔ x = y

Tactic:
rw [RelCat.Hom.rel_id]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.of_mul_right [CancelCommMonoidWithZero M] {a b c d : M} :
    a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c d : M
⊢ a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
rw [mul_comm a, mul_comm c]

Result:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
a b c d : M
⊢ b * a ~ᵤ d * c → b ~ᵤ d → b ≠ 0 → a ~ᵤ c

Tactic:
exact Associated.of_mul_left

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem kernelSubobject_factors {W : C} (h : W ⟶ X) (w : h ≫ f = 0) :
    (kernelSubobject f).Factors h :=
  ⟨kernel.lift _ h w, by simp⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ kernel.lift f h w ≫ (MonoOver.mk' (kernel.ι f)).arrow = h

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma transfiniteCompositionsOfShape_le_transfiniteCompositions
    (J : Type w) [LinearOrder J] [SuccOrder J] [OrderBot J] [WellFoundedLT J] :
    W.transfiniteCompositionsOfShape J ≤ transfiniteCompositions.{w} W

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
⊢ W.transfiniteCompositionsOfShape J ≤ transfiniteCompositions.{w, v, u} W

Tactic:
intro A B f hf

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f

Tactic:
exact ⟨_, _, _, _, _, hf⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ transfiniteCompositions.{w, v, u} W f

Tactic:
rw [transfiniteCompositions_iff]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
A B : C
f : A ⟶ B
hf : W.transfiniteCompositionsOfShape J f
⊢ ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem tmul_ite (x₁ : M) (x₂ : N) (P : Prop) [Decidable P] :
    (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ x₂ else 0

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ[R] x₂ else 0

Tactic:
split_ifs <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma c_relation_of_char_two : W.c₄ ^ 3 = W.c₆ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.c₄ ^ 3 = W.c₆ ^ 2

Tactic:
linear_combination -W.c_relation + 864 * W.Δ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_comp_heq {C} [Category C] {W X Y : C}
    (f : Y ⟶ X) (h : W = Y) : HEq (eqToHom h ≫ f) f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
W X Y : C
f : Y ⟶ X
h : W = Y
⊢ HEq (eqToHom h ≫ f) f

Tactic:
rw [← conj_eqToHom_iff_heq _ _ h rfl, eqToHom_refl, Category.comp_id]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_coe_self_inter (s t : Set α) :
    ((↑) : s → α) ⁻¹' (s ∩ t) = ((↑) : s → α) ⁻¹' t

Proof state:
α : Type u_1
s t : Set α
⊢ val ⁻¹' (s ∩ t) = val ⁻¹' t

Tactic:
rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_singleton_self (a : α) : count a [a] = 1

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ count a [a] = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem ruzsa_triangle_inequality_invMul_invMul_invMul (A B C : Finset G) :
    #B * #(A⁻¹ * C) ≤ #(B⁻¹ * A) * #(B⁻¹ * C)

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
⊢ #B * #(A⁻¹ * C) ≤ #(B⁻¹ * A) * #(B⁻¹ * C)

Tactic:
simpa [mul_comm, div_eq_mul_inv, ← map_op_mul, ← map_op_inv] using
  ruzsa_triangle_inequality_div_div_div (G := Gᵐᵒᵖ) (C.map opEquiv.toEmbedding)
    (B.map opEquiv.toEmbedding) (A.map opEquiv.toEmbedding)

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma reflection_dualMap_eq_coreflection :
    (P.reflection i).dualMap ∘ₗ P.toLin.flip = P.toLin.flip ∘ₗ P.coreflection i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
⊢ ↑(P.reflection i).dualMap ∘ₗ P.toLin.flip = P.toLin.flip ∘ₗ ↑(P.coreflection i)

Tactic:
ext n m

Result:
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
n : N
m : M
⊢ ((↑(P.reflection i).dualMap ∘ₗ P.toLin.flip) n) m = ((P.toLin.flip ∘ₗ ↑(P.coreflection i)) n) m

Proof state:
case h.h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i : ι
n : N
m : M
⊢ ((↑(P.reflection i).dualMap ∘ₗ P.toLin.flip) n) m = ((P.toLin.flip ∘ₗ ↑(P.coreflection i)) n) m

Tactic:
simp [map_sub, coreflection_apply, reflection_apply, mul_comm (P.toPerfectPairing m (P.coroot i))]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_div_iff' : a / b ≤ c / d ↔ a * d ≤ c * b

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp]
lemma eulerChar_orderDual [BoundedOrder α] : eulerChar 𝕜 αᵒᵈ = eulerChar 𝕜 α

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : BoundedOrder α
⊢ eulerChar 𝕜 αᵒᵈ = eulerChar 𝕜 α

Tactic:
simp [eulerChar, ← mu_toDual 𝕜 (α := α)]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem MeasurableSet.congr {s t : Set α} (hs : MeasurableSet s) (h : s = t) : MeasurableSet t

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : Set α
hs : MeasurableSet s
h : s = t
⊢ MeasurableSet t

Tactic:
rwa [← h]

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer"
products of the block matrices. -/
lemma fromCols_mul_fromRows [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
    (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
    fromCols A₁ A₂ * fromRows B₁ B₂ = (A₁ * B₁ + A₂ * B₂)

Proof state:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Tactic:
ext

Result:
case a
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
i✝ : m
j✝ : n
⊢ (A₁.fromCols A₂ * B₁.fromRows B₂) i✝ j✝ = (A₁ * B₁ + A₂ * B₂) i✝ j✝

Proof state:
case a
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
i✝ : m
j✝ : n
⊢ (A₁.fromCols A₂ * B₁.fromRows B₂) i✝ j✝ = (A₁ * B₁ + A₂ * B₂) i✝ j✝

Tactic:
simp [mul_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem tsub_lt_tsub_right_of_le (hc : AddLECancellable c) (h : c ≤ a) (h2 : a < b) :
    a - c < b - c

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a - c < b - c

Tactic:
apply hc.lt_tsub_of_add_lt_left

Result:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ c + (a - c) < b

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

Tactic:
rwa [add_tsub_cancel_of_le h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_average [IsFiniteMeasure μ] {f : α → β} :
    Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ :=
  (eq_or_ne μ 0).by_cases (fun h => by simp [h]) fun h =>
    integrable_smul_measure (ENNReal.inv_ne_zero.2 <| measure_ne_top _ _)
      (ENNReal.inv_ne_top.2 <| mt Measure.measure_univ_eq_zero.1 h)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup β
inst✝ : IsFiniteMeasure μ
f : α → β
h : μ = 0
⊢ Integrable f ((μ univ)⁻¹ • μ) ↔ Integrable f μ

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_singleton {a : ℝ} : volume ({a} : Set ℝ) = 0

Proof state:
a : ℝ
⊢ volume {a} = 0

Tactic:
simp [volume_val]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem eval_monoidalComp
    {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i}
    (e_η : η = η') (e_θ : θ = θ') (e_αθ : α.hom ≫ θ' = αθ) (e_ηαθ : η' ≫ αθ = ηαθ) :
    η ≫ α.hom ≫ θ = ηαθ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
f g h i : C
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
simp [e_η, e_θ, e_αθ, e_ηαθ]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem le_pure_iff {f : Filter α} {a : α} : f ≤ pure a ↔ {a} ∈ f

Proof state:
α : Type u_1
f : Filter α
a : α
⊢ f ≤ pure a ↔ {a} ∈ f

Tactic:
rw [← principal_singleton, le_principal_iff]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ico_succ_right_of_not_isMax (hb : ¬IsMax b) : Ico a (succ b) = Icc a b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc a b

Tactic:
rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/RestrictScalars.lean
theorem restrictScalars_eq_top_iff {p : Submodule R M} : restrictScalars S p = ⊤ ↔ p = ⊤

Proof state:
S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p : Submodule R M
⊢ restrictScalars S p = ⊤ ↔ p = ⊤

Tactic:
simp [SetLike.ext_iff]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsClosed.interior_union_right (h : IsClosed t) :
    interior (s ∪ t) ⊆ interior s ∪ t

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
h : IsClosed t
⊢ interior (s ∪ t) ⊆ interior s ∪ t

Tactic:
simpa only [union_comm _ t] using h.interior_union_left

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_vecMulVec (x : α) (v : Fin m → α) (w : n' → α) :
    vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)

Proof state:
case a
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ vecMulVec (vecCons x v) w i j✝ = vecCons (x • w) (vecMulVec v w) i j✝

Tactic:
refine Fin.cases ?_ ?_ i <;> simp [vecMulVec]

Result:
no goals

Proof state:
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
⊢ vecMulVec (vecCons x v) w = vecCons (x • w) (vecMulVec v w)

Tactic:
ext i

Result:
case a
α : Type u
m : ℕ
n' : Type uₙ
inst✝ : NonUnitalNonAssocSemiring α
x : α
v : Fin m → α
w : n' → α
i : Fin m.succ
j✝ : n'
⊢ vecMulVec (vecCons x v) w i j✝ = vecCons (x • w) (vecMulVec v w) i j✝
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
theorem ext_iff {M N : CStarMatrix m n A} : (∀ i j, M i j = N i j) ↔ M = N :=
  ⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
M N : CStarMatrix m n A
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_blsub_iff {o : Ordinal.{u}} {f : ∀ b < o, Ordinal.{max u v}} {a} :
    a < blsub.{_, v} o f ↔ ∃ i hi, a ≤ f i hi

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi

Tactic:
simpa only [not_forall, not_lt, not_le] using not_congr (@blsub_le_iff.{_, v} _ f a)

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem count_mul {a : Associates α} (ha : a ≠ 0) {b : Associates α}
    (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p) :
    count p (factors (a * b)) = count p a.factors + count p b.factors

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
⊢ p.count (Associates.mk a0 * b).factors = p.count (Associates.mk a0).factors + p.count b.factors

Tactic:
obtain ⟨b0, nzb, rfl⟩ := exists_non_zero_rep hb

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count (Associates.mk a0 * Associates.mk b0).factors =
    p.count (Associates.mk a0).factors + p.count (Associates.mk b0).factors

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a : Associates α
ha : a ≠ 0
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
⊢ p.count (a * b).factors = p.count a.factors + p.count b.factors

Tactic:
obtain ⟨a0, nza, rfl⟩ := exists_non_zero_rep ha

Result:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
⊢ p.count (Associates.mk a0 * b).factors = p.count (Associates.mk a0).factors + p.count b.factors

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
a0 : α
nza : a0 ≠ 0
ha : Associates.mk a0 ≠ 0
b0 : α
nzb : b0 ≠ 0
hb : Associates.mk b0 ≠ 0
⊢ p.count (Associates.mk a0 * Associates.mk b0).factors =
    p.count (Associates.mk a0).factors + p.count (Associates.mk b0).factors

Tactic:
rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp,
  Multiset.count_add, count_some hp, count_some hp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem and_and_left  : a ∧ (b ∧ c) ↔ (a ∧ b) ∧ a ∧ c

Proof state:
a b c : Prop
⊢ a ∧ b ∧ c ↔ (a ∧ b) ∧ a ∧ c

Tactic:
rw [and_and_and_comm, and_self]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Basic.lean
lemma inv_left_hom_right [IsIso e] : L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom

Proof state:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_modify_self (h : m.1.WF) {k : α} {f : β → β} :
    Const.get? (Const.modify m k f) k = (Const.get? m k).map f

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : β → β
⊢ get? (modify m k f) k = Option.map f (get? m k)

Tactic:
simp_to_model [Const.modify] using List.Const.getValue?_modifyKey_self

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
lemma image2_range (f : α' → β' → γ) (g : α → α') (h : β → β') :
    image2 f (range g) (range h) = range fun x : α × β ↦ f (g x.1) (h x.2)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
f : α' → β' → γ
g : α → α'
h : β → β'
⊢ image2 f (range g) (range h) = range fun x => f (g x.1) (h x.2)

Tactic:
simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]

Result:
no goals
-- Mathlib/Order/Filter/Pi.lean
theorem mem_coprodᵢ_iff {s : Set (∀ i, α i)} :
    s ∈ Filter.coprodᵢ f ↔ ∀ i : ι, ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ s

Proof state:
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
⊢ s ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), ∃ t₁ ∈ f i, eval i ⁻¹' t₁ ⊆ s

Tactic:
simp [Filter.coprodᵢ]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_spectrum_le (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σ 𝕜 a) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
a : A
x : 𝕜
hx : x ∈ σ 𝕜 a
ha : autoParam (p a) _auto✝
⊢ ‖x‖ ≤ ‖a‖

Tactic:
simpa only [cfc_id 𝕜 a] using norm_apply_le_norm_cfc (id : 𝕜 → 𝕜) a hx

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
lemma ChainComplex.exactAt_succ_single_obj (A : C) (n : ℕ) :
    ExactAt ((single₀ C).obj A) (n + 1) :=
  exactAt_single_obj _ _ _ _ (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A : C
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem mem_subtype {p : α → Prop} [DecidablePred p] {s : Finset α} :
    ∀ {a : Subtype p}, a ∈ s.subtype p ↔ (a : α) ∈ s
  | ⟨a, ha⟩ => by simp [Finset.subtype, ha]

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ ⟨a, ha⟩ ∈ Finset.subtype p s ↔ ↑⟨a, ha⟩ ∈ s

Tactic:
simp [Finset.subtype, ha]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidtNormed_unit_length_coe {f : ι → E} (n : ι)
    (h₀ : LinearIndependent 𝕜 (f ∘ ((↑) : Set.Iic n → ι))) : ‖gramSchmidtNormed 𝕜 f n‖ = 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
⊢ ‖gramSchmidtNormed 𝕜 f n‖ = 1

Tactic:
simp only [gramSchmidt_ne_zero_coe n h₀, gramSchmidtNormed, norm_smul_inv_norm, Ne,
  not_false_iff]

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/Basic.lean
theorem separableClosure.eq_bot_iff
    {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] :
    separableClosure F E = ⊥ ↔ IsPurelyInseparable F E :=
  ⟨fun h ↦ isPurelyInseparable_iff.2 fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, fun hs ↦ by
    simpa only [h] using mem_separableClosure_iff.2 hs⟩, fun _ ↦ eq_bot_of_isPurelyInseparable F E⟩

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : separableClosure F E = ⊥
x : E
hs : IsSeparable F x
⊢ x ∈ (algebraMap F E).range

Tactic:
simpa only [h] using mem_separableClosure_iff.2 hs

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem subset_bipolar (s : Set E) : s ⊆ B.flip.polar (B.polar s) := fun x hx y hy => by
  rw [B.flip_apply]
  exact hy x hx

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
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ ‖(B.flip y) x‖ ≤ 1

Tactic:
rw [B.flip_apply]

Result:
𝕜 : 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
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ ‖(B x) y‖ ≤ 1

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
hx : x ∈ s
y : F
hy : y ∈ B.polar s
⊢ ‖(B x) y‖ ≤ 1

Tactic:
exact hy x hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertManyIfNewUnit_empty_list_cons {hd : α} {tl : List α} :
    insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) (hd :: tl) =
      (insertManyIfNewUnit (empty.insertIfNew hd ()) tl).1

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α
tl : List α
⊢ (insertManyIfNewUnit empty (hd :: tl)).val = (insertManyIfNewUnit (empty.insertIfNew hd ()) tl).val

Tactic:
rw [insertManyIfNewUnit_cons]

Result:
no goals