harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
/-- The associativity compatibility for the extension of scalars, in the exact form
that is needed in the definition `CommRingCat.moduleCatExtendScalarsPseudofunctor`
in the file `Algebra.Category.ModuleCat.Pseudofunctor` -/
lemma extendScalars_assoc' :
    (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫ whiskerRight (extendScalarsComp f₁₂ f₂₃).hom _ ≫
      (Functor.associator _ _ _).hom ≫ whiskerLeft _ (extendScalarsComp f₂₃ f₃₄).inv ≫
        (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv = 𝟙 _

Proof state:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
      whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv ≫
          ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
            whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).inv ≫
              (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
simp only [Iso.inv_hom_id_assoc, ← whiskerLeft_comp_assoc, Iso.hom_inv_id,
  whiskerLeft_id', Category.id_comp]

Result:
no goals

Proof state:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
      whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄) ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
          whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).inv ≫ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
rw [extendScalars_assoc_assoc]

Result:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
      whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).hom ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv ≫
          ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
            whiskerLeft (extendScalars f₁₂) (extendScalarsComp f₂₃ f₃₄).inv ≫
              (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma isoClosure_eq_iff (P : MorphismProperty C) :
    P.isoClosure = P ↔ P.RespectsIso

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ P f

Tactic:
exact (P.arrow_mk_iso_iff e).1 hf'

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
⊢ P.isoClosure ≤ P

Tactic:
intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y : C
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk f' ≅ Arrow.mk f
⊢ P f
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Subalgebra.rank_top : Module.rank F (⊤ : Subalgebra F E) = Module.rank F E

Proof state:
F : Type u_2
E : Type u_3
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
⊢ Module.rank F ↥⊤ = Module.rank F E

Tactic:
exact _root_.rank_top F E

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem quasispectrum.algebraMap_mem_iff (S : Type*) {R A : Type*} [Semifield R] [Field S]
    [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A]
    [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} :
    algebraMap R S r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

Proof state:
S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

Tactic:
simp_rw [Unitization.quasispectrum_eq_spectrum_inr' _ S a, spectrum.algebraMap_mem_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem support_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : support (finRotate n) = Finset.univ

Proof state:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).support = Finset.univ

Tactic:
rw [add_comm, support_finRotate]

Result:
no goals

Proof state:
n : ℕ
h : 2 ≤ n
⊢ (finRotate n).support = Finset.univ

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Result:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).support = Finset.univ
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem lcm_union (s₁ s₂ : Multiset α) : (s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (s₁ ∪ s₂).lcm = GCDMonoid.lcm s₁.lcm s₂.lcm

Tactic:
rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_add]

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

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

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpIndSMul_smul (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : ℝ) (x : G) :
    condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ (c • x))) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) =
    c • (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))

Tactic:
rw [toSpanSingleton_smul, smul_compLpL, smul_apply]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ condExpIndSMul hm hs hμs (c • x) = c • condExpIndSMul hm hs hμs x

Tactic:
simp_rw [condExpIndSMul]

Result:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : ℝ
x : G
⊢ (compLpL 2 μ (toSpanSingleton ℝ (c • x))) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) =
    c • (compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condExpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))
-- Mathlib/Computability/TMConfig.lean
theorem cons_eval (f fs) : (cons f fs).eval = fun v => do {
    let n ← Code.eval f v
    let ns ← Code.eval fs v
    pure (n.headI :: ns) }

Proof state:
f fs : Code
⊢ (f.cons fs).eval = fun v => do
    let n ← f.eval v
    let ns ← fs.eval v
    pure (n.headI :: ns)

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitOpIsoOpColimit_inv_comp_π (F : J ⥤ C) [HasColimit F] (j : Jᵒᵖ) :
    (limitOpIsoOpColimit F).inv ≫ limit.π F.op j = (colimit.ι F j.unop).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ C
inst✝ : HasColimit F
j : Jᵒᵖ
⊢ (limitOpIsoOpColimit F).inv ≫ limit.π F.op j = (colimit.ι F (unop j)).op

Tactic:
simp [limitOpIsoOpColimit]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.bijective_costar_iff_bijective_star (u : U) :
    Bijective (φ.costar u) ↔ Bijective (φ.star u)

Proof state:
U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ Bijective (φ.costar u) ↔ Bijective (φ.star u)

Tactic:
rw [Prefunctor.costar_conj_star φ, EquivLike.comp_bijective, EquivLike.bijective_comp]

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) :
    ((Ico n m).filter fun x => x < l) = Ico n m :=
  filter_eq_self.2 fun k hk => by
    simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_true]

Proof state:
n m l : ℕ
hml : m ≤ l
k : ℕ
hk : k ∈ Ico n m
⊢ decide (k < l) = true

Tactic:
simp only [(lt_of_lt_of_le (mem.1 hk).2 hml), decide_true]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem cRk_le_iff : M.cRk X ≤ κ ↔ ∀ ⦃I⦄, M.IsBasis' I X → #I ≤ κ

Proof state:
α : Type u
M : Matroid α
X : Set α
κ : Cardinal.{u}
⊢ M.cRk X ≤ κ ↔ ∀ ⦃I : Set α⦄, M.IsBasis' I X → #↑I ≤ κ

Tactic:
simp_rw [cRk, cRank_le_iff, isBase_restrict_iff']

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem val_eq_zero_iff [NeZero n] {a : Fin n} : a.val = 0 ↔ a = 0

Proof state:
n : ℕ
inst✝ : NeZero n
a : Fin n
⊢ ↑a = 0 ↔ a = 0

Tactic:
rw [Fin.ext_iff, val_zero]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem closure_induction' (s : Set M) {p : ∀ x, x ∈ closure L s → Prop}
    (Hs : ∀ (x) (h : x ∈ s), p x (subset_closure h))
    (Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f { x | ∃ hx, p x hx }) {x}
    (hx : x ∈ closure L s) : p x hx

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc

Result:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ ∃ (x_1 : x ∈ (closure L).toFun s), p x x_1

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ ∃ (x_1 : x ∈ (closure L).toFun s), p x x_1

Tactic:
exact closure_induction hx (fun x hx => ⟨subset_closure hx, Hs x hx⟩) @Hfun

Result:
no goals
-- Mathlib/RepresentationTheory/Rep.lean
theorem ihom_ev_app_hom (A B : Rep k G) :
    Action.Hom.hom ((ihom.ev A).app B) = ModuleCat.ofHom
      (TensorProduct.uncurry k A (A →ₗ[k] B) B LinearMap.id.flip)

Proof state:
case hf.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B).V
⊢ (ModuleCat.Hom.hom ((ihom.ev A).app B).hom) x✝ =
    (ModuleCat.Hom.hom (ModuleCat.ofHom ((TensorProduct.uncurry k (↑A.V) (↑A.V →ₗ[k] ↑B.V) ↑B.V) LinearMap.id.flip))) x✝

Tactic:
rfl

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
⊢ ((ihom.ev A).app B).hom = ModuleCat.ofHom ((TensorProduct.uncurry k (↑A.V) (↑A.V →ₗ[k] ↑B.V) ↑B.V) LinearMap.id.flip)

Tactic:
ext

Result:
case hf.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B).V
⊢ (ModuleCat.Hom.hom ((ihom.ev A).app B).hom) x✝ =
    (ModuleCat.Hom.hom (ModuleCat.ofHom ((TensorProduct.uncurry k (↑A.V) (↑A.V →ₗ[k] ↑B.V) ↑B.V) LinearMap.id.flip))) x✝
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem mul_adjugate_apply (A : Matrix n n α) (i j k) :
    A i k * adjugate A k j = cramer Aᵀ (Pi.single k (A i k)) j

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j k : n
⊢ A i k * A.adjugate k j = Aᵀ.cramer (Pi.single k (A i k)) j

Tactic:
rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← LinearMap.map_smul, ← Pi.single_smul',
  smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
lemma eq_sqrt_of_sq_eq {B : Matrix n n 𝕜} (hB : PosSemidef B) (hAB : A ^ 2 = B) : A = hB.sqrt

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
B : Matrix n n 𝕜
hB : B.PosSemidef
hAB : A ^ 2 = B
⊢ A = hB.sqrt

Tactic:
subst B

Result:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
hB : (A ^ 2).PosSemidef
⊢ A = hB.sqrt

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝² : Fintype n
inst✝¹ : RCLike 𝕜
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.PosSemidef
hB : (A ^ 2).PosSemidef
⊢ A = hB.sqrt

Tactic:
rw [hA.sqrt_sq]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_compl (t : Set Ω) (hs : s.Finite) (hs' : s.Nonempty) :
    uniformOn s t + uniformOn s tᶜ = 1

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ (uniformOn s) t + (uniformOn s) tᶜ = 1

Tactic:
rw [← uniformOn_union hs disjoint_compl_right, Set.union_compl_self,
  (uniformOn_isProbabilityMeasure hs hs').measure_univ]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivWithinAt.smul (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
    HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s 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
s : Set E
𝕜' : Type u_5
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
hf : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) s x

Tactic:
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp_hasFDerivWithinAt x <|
  hc.prod hf

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
@[simp] lemma insertNthEquiv_zero (α : Fin (n + 1) → Type*) : insertNthEquiv α 0 = consEquiv α :=
  Equiv.symm_bijective.injective <| by ext <;> rfl

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_3
⊢ (insertNthEquiv α 0).symm = (consEquiv α).symm

Tactic:
ext <;> rfl

Result:
no goals
-- Mathlib/Algebra/QuaternionBasis.lean
theorem k_mul_j : q.k * q.j = c₃ • q.i

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.k * q.j = c₃ • q.i

Tactic:
rw [← i_mul_j, mul_assoc, j_mul_j, mul_smul_comm, mul_one]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NeZero.lean
theorem domain_nontrivial [Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f 0 = 0) (one : f 1 = 1) :
    Nontrivial M₀' :=
  ⟨⟨0, 1, mt (congr_arg f) <| by
    rw [zero, one]
    exact zero_ne_one⟩⟩

Proof state:
M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1

Tactic:
exact zero_ne_one

Result:
no goals

Proof state:
M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬f 0 = f 1

Tactic:
rw [zero, one]

Result:
M₀ : Type u_1
M₀' : Type u_2
inst✝³ : MulZeroOneClass M₀
inst✝² : Nontrivial M₀
inst✝¹ : Zero M₀'
inst✝ : One M₀'
f : M₀' → M₀
zero : f 0 = 0
one : f 1 = 1
⊢ ¬0 = 1
-- Mathlib/Data/Multiset/AddSub.lean
theorem card_erase_eq_ite {a : α} {s : Multiset α} :
    card (s.erase a) = if a ∈ s then pred (card s) else card s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∉ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∉ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
rwa [erase_of_not_mem h, if_neg]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
h : a ∈ s
⊢ (s.erase a).card = if a ∈ s then s.card.pred else s.card

Tactic:
rwa [card_erase_of_mem h, if_pos]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_coe_nat (n : ℕ) : toNNRat n = n :=
  ext <| by simp only [Nat.cast_nonneg', Rat.coe_toNNRat]; rfl

Proof state:
n : ℕ
⊢ ↑n = ↑↑n

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ ↑(↑n).toNNRat = ↑↑n

Tactic:
simp only [Nat.cast_nonneg', Rat.coe_toNNRat]

Result:
n : ℕ
⊢ ↑n = ↑↑n
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem sub_self {X Y : C} (a : X ⟶ Y) : a - a = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - a = 0

Tactic:
rw [sub_def, ← Category.comp_id a, ← prod.comp_lift, Category.assoc, diag_σ, comp_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive] lemma exists_mem_ne_one_of_prod_ne_one (h : l.prod ≠ 1) :
    ∃ x ∈ l, x ≠ (1 : M)

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List M
h : l.prod ≠ 1
⊢ ∃ x, x ∈ l ∧ x ≠ 1

Tactic:
simpa only [not_forall, exists_prop] using mt prod_eq_one h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem not_hasPos_removePos (assignment : Assignment) :
    ¬hasPosAssignment (removePosAssignment assignment)

Proof state:
assignment : Assignment
⊢ ¬assignment.removePosAssignment.hasPosAssignment = true

Tactic:
cases assignment <;> simp [removePosAssignment, hasPosAssignment]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPullback.iso_inv_fst :
    (PreservesPullback.iso G f g).inv ≫ G.map (pullback.fst f g) = pullback.fst _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map (pullback.fst f g) = pullback.fst (G.map f) (G.map g)

Tactic:
simp [PreservesPullback.iso, Iso.inv_comp_eq]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma in₀₁_iff : (graph t).Adj (in₀ a) (in₁ b) ↔ ∃ c, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₀₁ h⟩

Proof state:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
⊢ (graph t).Adj (in₀ a) (in₁ b) → ∃ c, (a, b, c) ∈ t

Tactic:
rintro ⟨⟩

Result:
case in₀₁
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c✝ : γ
a✝ : (a, b, c✝) ∈ t
⊢ ∃ c, (a, b, c) ∈ t
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_div_sin_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Tactic:
rcases h0 with (h0 | h0)

Result:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Proof state:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Tactic:
simp [h0]

Result:
no goals

Proof state:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖

Tactic:
rw [sin_angle_add_of_inner_eq_zero h (Or.inr h0), div_div_eq_mul_div, mul_comm, div_eq_mul_inv,
  mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_succ' (f : ℕ → β) :
    ∀ n : ℕ, (∏ k ∈ range (n + 1), f k) = (∏ k ∈ range n, f (k + 1)) * f 0
  | 0 => prod_range_succ _ _
  | n + 1 => by rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0

Tactic:
rw [prod_range_succ _ n, mul_right_comm, ← prod_range_succ' _ n, prod_range_succ]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
protected lemma mul_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a * b :=
  numDenCasesOn' a fun n₁ d₁ h₁ =>
    numDenCasesOn' b fun n₂ d₂ h₂ => by
      have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁
      have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂
      simp only [d₁0, d₂0, Int.mul_pos, divInt_nonneg_iff_of_pos_right,
        divInt_mul_divInt _ _ d₁0.ne' d₂0.ne']
      apply Int.mul_nonneg

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)

Tactic:
have d₂0 : 0 < (d₂ : ℤ) := mod_cast Nat.pos_of_ne_zero h₂

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)

Tactic:
simp only [d₁0, d₂0, Int.mul_pos, divInt_nonneg_iff_of_pos_right,
  divInt_mul_divInt _ _ d₁0.ne' d₂0.ne']

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * n₂

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)

Tactic:
have d₁0 : 0 < (d₁ : ℤ) := mod_cast Nat.pos_of_ne_zero h₁

Result:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
⊢ 0 ≤ n₁ /. ↑d₁ → 0 ≤ n₂ /. ↑d₂ → 0 ≤ n₁ /. ↑d₁ * (n₂ /. ↑d₂)

Proof state:
a b : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
d₁0 : 0 < ↑d₁
d₂0 : 0 < ↑d₂
⊢ 0 ≤ n₁ → 0 ≤ n₂ → 0 ≤ n₁ * n₂

Tactic:
apply Int.mul_nonneg

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_Icc_pi_toReal {a b : ι → ℝ} (h : a ≤ b) :
    (volume (Icc a b)).toReal = ∏ i, (b i - a i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (Icc a b)).toReal = ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_Icc_pi, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem top_symmDiff' : ⊤ ∆ a = ￢a

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ∆ a = ￢a

Tactic:
simp [symmDiff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem _root_.Int.addLeft_one_isCycle : (Equiv.addLeft 1 : Perm ℤ).IsCycle :=
  ⟨0, one_ne_zero, fun n _ => ⟨n, by simp⟩⟩

Proof state:
n : ℤ
x✝ : (Equiv.addLeft 1) n ≠ n
⊢ (Equiv.addLeft 1 ^ n) 0 = n

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ioo_left (f : ∀ i, α i) (i : ι) (a : α i) :
    update f i '' Ioo a (f i) = Ioo (update f i a) f

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioo a (f i) = Ioo (update f i a) f

Tactic:
simpa using image_update_Ioo f i a (f i)

Result:
no goals