harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicTopology/SimplicialNerve.lean
@[simp]
lemma assoc (i j k l : SimplicialThickening J) :
    (α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l =
      Hom i j ◁ comp j k l ≫ comp i j l

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j k l : SimplicialThickening J
⊢ (α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l = Hom i j ◁ comp j k l ≫ comp i j l

Tactic:
ext

Result:
case w.h
J : Type u_1
inst✝ : LinearOrder J
i j k l : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (Hom i j ⊗ Hom j k ⊗ Hom k l).obj n✝
⊢ ((α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l).app n✝ a✝ =
    (Hom i j ◁ comp j k l ≫ comp i j l).app n✝ a✝

Proof state:
case w.h
J : Type u_1
inst✝ : LinearOrder J
i j k l : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (Hom i j ⊗ Hom j k ⊗ Hom k l).obj n✝
⊢ ((α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l).app n✝ a✝ =
    (Hom i j ◁ comp j k l ≫ comp i j l).app n✝ a✝

Tactic:
exact Functor.ext (fun _ ↦ by simp)

Result:
no goals

Proof state:
J : Type u_1
inst✝ : LinearOrder J
i j k l : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (Hom i j ⊗ Hom j k ⊗ Hom k l).obj n✝
x✝ : Fin ((Opposite.unop n✝).len + 1)
⊢ (((α_ (Hom i j) (Hom j k) (Hom k l)).inv ≫ comp i j k ▷ Hom k l ≫ comp i k l).app n✝ a✝).obj x✝ =
    ((Hom i j ◁ comp j k l ≫ comp i j l).app n✝ a✝).obj x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Complex/Module.lean
theorem realPart_smul (z : ℂ) (a : A) : ℜ (z • a) = z.re • ℜ a - z.im • ℑ a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ℜ (z • a) = z.re • ℜ a - z.im • ℑ a

Tactic:
have := by congrm (ℜ ($((re_add_im z).symm) • a))

Result:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
this : ℜ (z • a) = ℜ ((↑z.re + ↑z.im * I) • a)
⊢ ℜ (z • a) = z.re • ℜ a - z.im • ℑ a

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ?m.158343

Tactic:
congrm (ℜ ($((re_add_im z).symm) • a))

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
this : ℜ (z • a) = ℜ ((↑z.re + ↑z.im * I) • a)
⊢ ℜ (z • a) = z.re • ℜ a - z.im • ℑ a

Tactic:
simpa [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast_iota (n : Nat) (h) : (iota n).getLast h = 1

Proof state:
n : Nat
h : iota n ≠ []
⊢ (iota n).getLast h = 1

Tactic:
rw [getLast_eq_head_reverse]

Result:
n : Nat
h : iota n ≠ []
⊢ (iota n).reverse.head ⋯ = 1

Proof state:
n : Nat
h : iota n ≠ []
⊢ (iota n).reverse.head ⋯ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
@[reassoc]
lemma toOpen_toSpec_val_c_app (f) (U) :
    StructureSheaf.toOpen (A⁰_ f) U.unop ≫ (toSpec 𝒜 f).c.app U =
      awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.map (homOfLE le_top).op :=
  Eq.trans (by congr) <| ΓSpec.toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app _ U

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
U : (Opens ↑↑(Spec A⁰_ f).toPresheafedSpace)ᵒᵖ
⊢ StructureSheaf.toOpen (A⁰_ f) (unop U) ≫ (toSpec 𝒜 f).c.app U =
    StructureSheaf.toOpen (A⁰_ f) (unop U) ≫
      ((ΓSpec.locallyRingedSpaceAdjunction.homEquiv (Proj.restrict ⋯) (op (CommRingCat.of (A⁰_ f))))
              (awayToΓ 𝒜 f).op).c.app
        U

Tactic:
congr

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem le_div {a b c : Ordinal} (c0 : c ≠ 0) : a ≤ b / c ↔ c * a ≤ b

Proof state:
case H₃
b c : Ordinal.{u_4}
c0 : c ≠ 0
o✝ : Ordinal.{u_4}
h₁ : o✝.IsLimit
h₂ : ∀ o' < o✝, o' ≤ b / c ↔ c * o' ≤ b
⊢ o✝ ≤ b / c ↔ c * o✝ ≤ b

Tactic:
revert h₁ h₂

Result:
case H₃
b c : Ordinal.{u_4}
c0 : c ≠ 0
o✝ : Ordinal.{u_4}
⊢ o✝.IsLimit → (∀ o' < o✝, o' ≤ b / c ↔ c * o' ≤ b) → (o✝ ≤ b / c ↔ c * o✝ ≤ b)

Proof state:
a b c : Ordinal.{u_4}
c0 : c ≠ 0
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
induction a using limitRecOn with
| H₁ => simp only [mul_zero, Ordinal.zero_le]
| H₂ _ _ => rw [succ_le_iff, lt_div c0]
| H₃ _ h₁ h₂ =>
  revert h₁ h₂
  simp +contextual only [mul_le_of_limit, limit_le, forall_true_iff]

Result:
no goals

Proof state:
case H₃
b c : Ordinal.{u_4}
c0 : c ≠ 0
o✝ : Ordinal.{u_4}
⊢ o✝.IsLimit → (∀ o' < o✝, o' ≤ b / c ↔ c * o' ≤ b) → (o✝ ≤ b / c ↔ c * o✝ ≤ b)

Tactic:
simp +contextual only [mul_le_of_limit, limit_le, forall_true_iff]

Result:
no goals

Proof state:
case H₂
b c : Ordinal.{u_4}
c0 : c ≠ 0
o✝ : Ordinal.{u_4}
a✝ : o✝ ≤ b / c ↔ c * o✝ ≤ b
⊢ succ o✝ ≤ b / c ↔ c * succ o✝ ≤ b

Tactic:
rw [succ_le_iff, lt_div c0]

Result:
no goals

Proof state:
case H₁
b c : Ordinal.{u_4}
c0 : c ≠ 0
⊢ 0 ≤ b / c ↔ c * 0 ≤ b

Tactic:
simp only [mul_zero, Ordinal.zero_le]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem to_of_int (n : ℤ) : ((n : ZNum) : ℤ) = n :=
  Int.inductionOn' n 0 (by simp) (by simp) (by simp)

Proof state:
n : ℤ
⊢ ∀ (k : ℤ), 0 ≤ k → ↑↑k = k → ↑↑(k + 1) = k + 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℤ
⊢ ↑↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
n : ℤ
⊢ ∀ k ≤ 0, ↑↑k = k → ↑↑(k - 1) = k - 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_const_mul_le (r : ℝ≥0∞) (f : α → ℝ≥0∞) :
    r * ∫⁻ a, f a ∂μ ≤ ∫⁻ a, r * f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ r * ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [lintegral, ENNReal.mul_iSup]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ⨆ i, r * ⨆ (_ : ⇑i ≤ fun a => f a), i.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ⇑s ≤ fun a => f a
⊢ (const α r * s).lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => r * f a), g.lintegral μ

Tactic:
refine le_iSup_of_le (const α r * s) (le_iSup_of_le (fun x => ?_) le_rfl)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ⇑s ≤ fun a => f a
x : α
⊢ (const α r * s) x ≤ (fun a => r * f a) x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ⇑s ≤ fun a => f a
⊢ r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [← SimpleFunc.const_mul_lintegral, lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ⇑s ≤ fun a => f a
⊢ (const α r * s).lintegral μ ≤ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => r * f a), g.lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ r * ⨆ (_ : ⇑s ≤ fun a => f a), s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
rw [ENNReal.mul_iSup, iSup_le_iff]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (⇑s ≤ fun a => f a) → r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ (⇑s ≤ fun a => f a) → r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
intro hs

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ⇑s ≤ fun a => f a
⊢ r * s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
hs : ⇑s ≤ fun a => f a
x : α
⊢ (const α r * s) x ≤ (fun a => r * f a) x

Tactic:
exact mul_le_mul_left' (hs x) _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ⨆ i, r * ⨆ (_ : ⇑i ≤ fun a => f a), i.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ

Tactic:
refine iSup_le fun s => ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
s : α →ₛ ℝ≥0∞
⊢ r * ⨆ (_ : ⇑s ≤ fun a => f a), s.lintegral μ ≤ ∫⁻ (a : α), r * f a ∂μ
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma Δ_of_char_three : W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3

Tactic:
linear_combination (-9 * W.b₆ ^ 2 + 3 * W.b₂ * W.b₄ * W.b₆) * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.Δ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3

Tactic:
rw [Δ]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3 - 27 * W.b₆ ^ 2 + 9 * W.b₂ * W.b₄ * W.b₆ = -W.b₂ ^ 2 * W.b₈ - 8 * W.b₄ ^ 3
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem eqOn_or_eventually_ne_of_preconnected (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
    (hU : IsPreconnected U) : EqOn f g U ∨ ∀ᶠ x in codiscreteWithin U, f x ≠ g x :=
  (eqOn_zero_or_eventually_ne_zero_of_preconnected (hf.sub hg) hU).imp
    (fun h _ hx ↦ eq_of_sub_eq_zero (h hx))
    (by simp only [Pi.sub_apply, ne_eq, sub_eq_zero, imp_self])

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
⊢ (∀ᶠ (x : 𝕜) in codiscreteWithin U, (f - g) x ≠ 0) → ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ g x

Tactic:
simp only [Pi.sub_apply, ne_eq, sub_eq_zero, imp_self]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma cyclesMap_comm [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    cyclesMap φ ≫ h₂.cyclesIso.hom = h₁.cyclesIso.hom ≫ γ.φK

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ cyclesMap φ ≫ h₂.cyclesIso.hom = h₁.cyclesIso.hom ≫ γ.φK

Tactic:
simp only [γ.cyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem minFac_one : minFac 1 = 1

Proof state:
⊢ minFac 1 = 1

Tactic:
simp [minFac, minFacAux]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_eq_isSome_getEntry? [BEq α] {l : List ((a : α) × β a)} {a : α} :
    containsKey a l = (getEntry? a l).isSome

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
⊢ containsKey a [] = (getEntry? a []).isSome

Tactic:
simp

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : containsKey a l = (getEntry? a l).isSome
h : (k == a) = false
⊢ containsKey a (⟨k, v⟩ :: l) = (getEntry? a (⟨k, v⟩ :: l)).isSome

Tactic:
simp [getEntry?_cons_of_false h, h, ih]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
⊢ containsKey a l = (getEntry? a l).isSome

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
⊢ containsKey a [] = (getEntry? a []).isSome

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey a tail✝ = (getEntry? a tail✝).isSome
⊢ containsKey a (⟨k✝, v✝⟩ :: tail✝) = (getEntry? a (⟨k✝, v✝⟩ :: tail✝)).isSome

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : containsKey a l = (getEntry? a l).isSome
h : (k == a) = true
⊢ containsKey a (⟨k, v⟩ :: l) = (getEntry? a (⟨k, v⟩ :: l)).isSome

Tactic:
simp [getEntry?_cons_of_true h, h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : containsKey a l = (getEntry? a l).isSome
⊢ containsKey a (⟨k, v⟩ :: l) = (getEntry? a (⟨k, v⟩ :: l)).isSome

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : containsKey a l = (getEntry? a l).isSome
h : (k == a) = false
⊢ containsKey a (⟨k, v⟩ :: l) = (getEntry? a (⟨k, v⟩ :: l)).isSome

case true
α : Type u
β : α → Type v
inst✝ : BEq α
a k : α
v : β k
l : List ((a : α) × β a)
ih : containsKey a l = (getEntry? a l).isSome
h : (k == a) = true
⊢ containsKey a (⟨k, v⟩ :: l) = (getEntry? a (⟨k, v⟩ :: l)).isSome
-- Mathlib/Order/Compare.lean
theorem toDual_compares_toDual [LT α] {a b : α} {o : Ordering} :
    Compares o (toDual a) (toDual b) ↔ Compares o b a

Proof state:
α : Type u_1
inst✝ : LT α
a b : α
o : Ordering
⊢ o.Compares (toDual a) (toDual b) ↔ o.Compares b a

Tactic:
cases o

Result:
case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.Compares (toDual a) (toDual b) ↔ lt.Compares b a

case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.Compares (toDual a) (toDual b) ↔ eq.Compares b a

case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.Compares (toDual a) (toDual b) ↔ gt.Compares b a

Proof state:
case lt
α : Type u_1
inst✝ : LT α
a b : α
⊢ lt.Compares (toDual a) (toDual b) ↔ lt.Compares b a

case eq
α : Type u_1
inst✝ : LT α
a b : α
⊢ eq.Compares (toDual a) (toDual b) ↔ eq.Compares b a

case gt
α : Type u_1
inst✝ : LT α
a b : α
⊢ gt.Compares (toDual a) (toDual b) ↔ gt.Compares b a

Tactic:
exacts [Iff.rfl, eq_comm, Iff.rfl]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_mul_distrib_aux (A B : Matrix n n α) (hA : IsLeftRegular A.det)
    (hB : IsLeftRegular B.det) : adjugate (A * B) = adjugate B * adjugate A

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
have hAB : IsLeftRegular (A * B).det := by
  rw [det_mul]
  exact hA.mul hB

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (fun x => A * B * x) (A * B).adjugate = (fun x => A * B * x) (B.adjugate * A.adjugate)

Tactic:
simp only

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (A * B).adjugate = B.adjugate * A.adjugate

Tactic:
refine (isRegular_of_isLeftRegular_det hAB).left ?_

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ (fun x => A * B * x) (A * B).adjugate = (fun x => A * B * x) (B.adjugate * A.adjugate)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ IsLeftRegular (A.det * B.det)

Tactic:
exact hA.mul hB

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ IsLeftRegular (A * B).det

Tactic:
rw [det_mul]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
⊢ IsLeftRegular (A.det * B.det)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
hA : IsLeftRegular A.det
hB : IsLeftRegular B.det
hAB : IsLeftRegular (A * B).det
⊢ A * B * (A * B).adjugate = A * B * (B.adjugate * A.adjugate)

Tactic:
rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,
  smul_mul, Matrix.one_mul, mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma fst_swapRight (κ : Kernel α (β × γ)) : fst (swapRight κ) = snd κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ.swapRight.fst a) s = (κ.snd a) s

Tactic:
rw [fst_apply' _ _ hs, swapRight_apply', snd_apply' _ _ hs]

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ a) {p | p.swap ∈ {p | p.1 ∈ s}} = (κ a) {p | p.2 ∈ s}

case h.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.swapRight.fst = κ.snd

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ.swapRight.fst a) s = (κ.snd a) s

Proof state:
case h.h.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet {p | p.1 ∈ s}

Tactic:
exact measurable_fst hs

Result:
no goals

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set γ
hs : MeasurableSet s
⊢ (κ a) {p | p.swap ∈ {p | p.1 ∈ s}} = (κ a) {p | p.2 ∈ s}

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem generator_submoduleImage_dvd_of_mem {N O : Submodule R M} (hNO : N ≤ O) (ϕ : O →ₗ[R] R)
    [(ϕ.submoduleImage N).IsPrincipal] {x : M} (hx : x ∈ N) :
    generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, hNO hx⟩

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
inst✝ : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ y, ∃ (yN : y ∈ N), ϕ ⟨y, ⋯⟩ = ϕ ⟨x, ⋯⟩

Tactic:
exact ⟨x, hx, rfl⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
inst✝ : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩

Tactic:
rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]

Result:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
inst✝ : (ϕ.submoduleImage N).IsPrincipal
x : M
hx : x ∈ N
⊢ ∃ y, ∃ (yN : y ∈ N), ϕ ⟨y, ⋯⟩ = ϕ ⟨x, ⋯⟩
-- Mathlib/Data/List/Sym.lean
theorem sym2_eq_nil_iff {xs : List α} : xs.sym2 = [] ↔ xs = []

Proof state:
α : Type u_1
xs : List α
⊢ xs.sym2 = [] ↔ xs = []

Tactic:
cases xs <;> simp [List.sym2]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem eq_of_forall_toMeasure_apply_eq (μ ν : FiniteMeasure Ω)
    (h : ∀ s : Set Ω, MeasurableSet s → (μ : Measure Ω) s = (ν : Measure Ω) s) : μ = ν

Proof state:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ ↑μ = ↑ν

Tactic:
ext1 s s_mble

Result:
case a.h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s

Proof state:
case a.h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s

Tactic:
exact h s s_mble

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ μ = ν

Tactic:
apply Subtype.ext

Result:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ ↑μ = ↑ν
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_mul_relrank_eq_inf_relrank (h : B ≤ C) :
    relrank A B * relrank B C = (A ⊓ B).relrank C

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Result:
no goals
-- Mathlib/Topology/Algebra/ProperAction/Basic.lean
theorem t2Space_quotient_mulAction_of_properSMul [ProperSMul G X] :
    T2Space (Quotient (MulAction.orbitRel G X))

Proof state:
case h.e'_3.h.mk
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
⊢ π x₁ = π x₂ ↔ ∃ a, a • x₂ = x₁

Tactic:
rw [Quotient.eq', MulAction.orbitRel_apply, MulAction.mem_orbit_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma radical_sup {I J : IdealSheafData X} :
    radical (I ⊔ J) = radical (radical I ⊔ radical J)

Proof state:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

Tactic:
ext U : 2

Result:
case ideal.h
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U

Proof state:
case ideal.h
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U

Tactic:
exact (Ideal.radical_sup (I.ideal U) (J.ideal U))

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.card_small_parts_eq_mod (hP : P.IsEquipartition) :
    #{p ∈ P.parts | #p = #s / #P.parts} = #P.parts - #s % #P.parts

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #(filter (fun p => #p = #s / #P.parts) P.parts) =
    #(filter (fun p => #p = #s / #P.parts + 1) P.parts) + #(filter (fun a => ¬#a = #s / #P.parts + 1) P.parts) -
      #s % #P.parts

Tactic:
rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #(filter (fun p => #p = #s / #P.parts) P.parts) = #P.parts - #s % #P.parts

Tactic:
conv_rhs =>
  arg 1
  rw [← filter_card_add_filter_neg_card_eq_card (p := fun p ↦ #p = #s / #P.parts + 1)]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ #(filter (fun p => #p = #s / #P.parts) P.parts) =
    #(filter (fun p => #p = #s / #P.parts + 1) P.parts) + #(filter (fun a => ¬#a = #s / #P.parts + 1) P.parts) -
      #s % #P.parts