harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem decompId_p_naturality {P Q : Karoubi C} (f : P ⟶ Q) :
    decompId_p P ≫ f = (by exact Hom.mk f.f (by simp)) ≫ decompId_p Q

Proof state:
C : Type u_1
inst✝ : Category.{?u.42651, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p ≫ f.f ≫ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }.p

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.42651, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ } ⟶ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }

Tactic:
exact Hom.mk f.f (by simp)

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ P.decompId_p ≫ f = { f := f.f, comm := ⋯ } ≫ Q.decompId_p

Tactic:
simp

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

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

Tactic:
simp_to_model [Const.alter] using List.Const.getKey_alterKey

Result:
no goals

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
inst✝ : Inhabited α
k k' : α
h : m.val.WF
f : Option β → Option β
hc : (alter m k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_alter _ h, if_neg heq] at hc

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma comp_contractNth {β : Sort*} (opα : α → α → α) (opβ : β → β → β) {f : α → β}
    (hf : ∀ x y, f (opα x y) = opβ (f x) (f y)) (j : Fin (n + 1)) (g : Fin (n + 1) → α) :
    f ∘ contractNth j opα g = contractNth j opβ (f ∘ g)

Proof state:
case h
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
rcases lt_trichotomy (x : ℕ) j with (h|h|h)

Result:
case h.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x < ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

case h.inr.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x = ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

case h.inr.inr
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑j < ↑x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Proof state:
case h.inr.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x = ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]

Result:
no goals

Proof state:
case h.inr.inr
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑j < ↑x
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_gt, h]

Result:
no goals

Proof state:
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
⊢ f ∘ j.contractNth opα g = j.contractNth opβ (f ∘ g)

Tactic:
ext x

Result:
case h
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Proof state:
case h.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x < ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_lt, h]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem liftIco_zero_coe_apply {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Ico 0 p) : liftIco p 0 f ↑x = f x :=
  liftIco_coe_apply (by rwa [zero_add])

Proof state:
𝕜 : Type u_1
B : Type u_2
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)

Tactic:
rwa [zero_add]

Result:
no goals
-- Mathlib/Logic/Nontrivial/Defs.lean
theorem not_nontrivial_iff_subsingleton : ¬Nontrivial α ↔ Subsingleton α

Proof state:
α : Type u_1
⊢ ¬Nontrivial α ↔ Subsingleton α

Tactic:
simp only [nontrivial_iff, subsingleton_iff, not_exists, Classical.not_not]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
lemma ringHomComp_pow (χ : MulChar R R') (f : R' →+* R'') (n : ℕ) :
    χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
n : ℕ
⊢ χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f

Tactic:
induction n with
| zero => simp only [pow_zero, ringHomComp_one]
| succ n ih => simp only [pow_succ, ih, ringHomComp_mul]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
n : ℕ
ih : χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
⊢ χ.ringHomComp f ^ (n + 1) = (χ ^ (n + 1)).ringHomComp f

Tactic:
simp only [pow_succ, ih, ringHomComp_mul]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
⊢ χ.ringHomComp f ^ 0 = (χ ^ 0).ringHomComp f

Tactic:
simp only [pow_zero, ringHomComp_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.toSubtype_fromSubtype [DecidablePred p] :
    biproduct.toSubtype f p ≫ biproduct.fromSubtype f p =
      biproduct.map fun j => if p j then 𝟙 (f j) else 0

Proof state:
case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
h : ¬p i
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j => if p j then 𝟙 (f j) else 0) ≫ π f i

Tactic:
simp [h]

Result:
no goals

Proof state:
case w
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j => if p j then 𝟙 (f j) else 0) ≫ π f i

Tactic:
by_cases h : p i

Result:
case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
h : p i
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j => if p j then 𝟙 (f j) else 0) ≫ π f i

case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
h : ¬p i
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j => if p j then 𝟙 (f j) else 0) ≫ π f i

Proof state:
case pos
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
h : p i
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j => if p j then 𝟙 (f j) else 0) ≫ π f i

Tactic:
simp [h]

Result:
no goals

Proof state:
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
⊢ toSubtype f p ≫ fromSubtype f p = map fun j => if p j then 𝟙 (f j) else 0

Tactic:
ext1 i

Result:
case w
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
i : J
⊢ (toSubtype f p ≫ fromSubtype f p) ≫ π f i = (map fun j => if p j then 𝟙 (f j) else 0) ≫ π f i
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem measurable_rnDeriv (μ ν : Measure α) : Measurable <| μ.rnDeriv ν

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable 0

Tactic:
exact measurable_zero

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
exact (haveLebesgueDecomposition_spec μ ν).1

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ Measurable (μ.rnDeriv ν)

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
rw [rnDeriv_of_not_haveLebesgueDecomposition h]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable 0
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma cube_of_not_dvd {n : ℤ} (h : ¬ 3 ∣ n) :
    (n : ZMod 9) ^ 3 = 1 ∨ (n : ZMod 9) ^ 3 = 8

Proof state:
n : ℤ
h : ¬3 ∣ n
⊢ ↑n ^ 3 = 1 ∨ ↑n ^ 3 = 8

Tactic:
apply cube_of_castHom_ne_zero

Result:
case a
n : ℤ
h : ¬3 ∣ n
⊢ (castHom ⋯ (ZMod 3)) ↑n ≠ 0

Proof state:
case a
n : ℤ
h : ¬3 ∣ n
⊢ (castHom ⋯ (ZMod 3)) ↑n ≠ 0

Tactic:
rwa [map_intCast, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem mem_ball_zero : y ∈ ball p 0 r ↔ p y < r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
y : E
r : ℝ
⊢ y ∈ p.ball 0 r ↔ p y < r

Tactic:
rw [mem_ball, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem derivedLength_eq_derivedLengthOfIdeal (I : LieIdeal R L) :
    derivedLength R I = derivedLengthOfIdeal R L I

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ derivedLength R ↥I = derivedLengthOfIdeal R L I

Tactic:
let s₁ := { k | derivedSeries R I k = ⊥ }

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
⊢ derivedLength R ↥I = derivedLengthOfIdeal R L I

Proof state:
case e_a.h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
⊢ k ∈ s₁ ↔ k ∈ s₂

Tactic:
exact I.derivedSeries_eq_bot_iff k

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLength R ↥I = derivedLengthOfIdeal R L I

Tactic:
change sInf s₁ = sInf s₂

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s₁ = sInf s₂

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
⊢ derivedLength R ↥I = derivedLengthOfIdeal R L I

Tactic:
let s₂ := { k | derivedSeriesOfIdeal R L k I = ⊥ }

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ derivedLength R ↥I = derivedLengthOfIdeal R L I

Proof state:
case e_a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s₁ = s₂

Tactic:
ext k

Result:
case e_a.h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
k : ℕ
⊢ k ∈ s₁ ↔ k ∈ s₂

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ sInf s₁ = sInf s₂

Tactic:
congr

Result:
case e_a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
s₁ : Set ℕ := {k | derivedSeries R (↥I) k = ⊥}
s₂ : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}
⊢ s₁ = s₂
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem dvd_gcd {a b c : R} : c ∣ a → c ∣ b → c ∣ gcd a b :=
  GCD.induction a b (fun _ _ H => by simpa only [gcd_zero_left] using H) fun a b _ IH ca cb => by
    rw [gcd_val]
    exact IH ((dvd_mod_iff ca).2 cb) ca

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a

Tactic:
exact IH ((dvd_mod_iff ca).2 cb) ca

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd a b

Tactic:
rw [gcd_val]

Result:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a✝ b✝ c a b : R
x✝ : a ≠ 0
IH : c ∣ b % a → c ∣ a → c ∣ gcd (b % a) a
ca : c ∣ a
cb : c ∣ b
⊢ c ∣ gcd (b % a) a

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b c x✝¹ : R
x✝ : c ∣ 0
H : c ∣ x✝¹
⊢ c ∣ gcd 0 x✝¹

Tactic:
simpa only [gcd_zero_left] using H

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_not (b : Bool) : (!!b) = b

Proof state:
b : Bool
⊢ (!!b) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem iInf_toSubmodule {ι : Sort*} (S : ι → NonUnitalSubalgebra R A) :
    (⨅ i, S i).toSubmodule = ⨅ i, (S i).toSubmodule :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i).toSubmodule = ↑(⨅ i, (S i).toSubmodule)

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Basic.lean
@[simp] lemma beq_eq_beq {α β : Type*} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {a₁ a₂ : α}
    {b₁ b₂ : β} : (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ (a₁ == a₂) = (b₁ == b₂) ↔ (a₁ = a₂ ↔ b₁ = b₂)

Tactic:
rw [Bool.eq_iff_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
a₁ a₂ : α
b₁ b₂ : β
⊢ ((a₁ == a₂) = true ↔ (b₁ == b₂) = true) ↔ (a₁ = a₂ ↔ b₁ = b₂)
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive
    [Nontrivial X] [IsPreprimitive G X] (a : X) :
    IsCoatom (stabilizer G a)

Proof state:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : Nontrivial X
inst✝ : IsPreprimitive G X
a : X
⊢ IsCoatom (stabilizer G a)

Tactic:
rwa [isCoatom_stabilizer_iff_preprimitive]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem eq_top_iff {S : Subalgebra R A} : S = ⊤ ↔ ∀ x : A, x ∈ S :=
  ⟨fun h x => by rw [h]; exact mem_top, fun h => by
    ext x; exact ⟨fun _ => mem_top, fun _ => h x⟩⟩

Proof state:
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
⊢ S = ⊤

Tactic:
ext x

Result:
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
rw [h]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤

Tactic:
exact mem_top

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
theorem counit_T (n : ℤ) :
    Coalgebra.counit (R := R) (T n : A[T;T⁻¹]) = 1

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Bialgebra R A
n : ℤ
⊢ CoalgebraStruct.counit (T n) = 1

Tactic:
simp [T, -single_eq_C_mul_T]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem IsPreconnected.iUnion_of_chain {s : β → Set α} (H : ∀ n, IsPreconnected (s n))
    (K : ∀ n, (s n ∩ s (succ n)).Nonempty) : IsPreconnected (⋃ n, s n) :=
  IsPreconnected.iUnion_of_reflTransGen H fun _ _ =>
    reflTransGen_of_succ _ (fun i _ => K i) fun i _ => by
      rw [inter_comm]
      exact K i

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝² x✝¹ i : β
x✝ : i ∈ Ico x✝¹ x✝²
⊢ (s i ∩ s (succ i)).Nonempty

Tactic:
exact K i

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝² x✝¹ i : β
x✝ : i ∈ Ico x✝¹ x✝²
⊢ (s (succ i) ∩ s i).Nonempty

Tactic:
rw [inter_comm]

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
H : ∀ (n : β), IsPreconnected (s n)
K : ∀ (n : β), (s n ∩ s (succ n)).Nonempty
x✝² x✝¹ i : β
x✝ : i ∈ Ico x✝¹ x✝²
⊢ (s i ∩ s (succ i)).Nonempty
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_const_smul (c : 𝕜) (f : α → F) (p : ℝ≥0∞) (μ : Measure α):
    eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Proof state:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (0 • f) p μ = ‖0‖ₑ * eLpNorm f p μ

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
refine le_antisymm eLpNorm_const_smul_le <| ENNReal.mul_le_of_le_div' ?_

Result:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
f : α → F
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (0 • f) p μ = ‖0‖ₑ * eLpNorm f p μ

case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm (c • f) p μ = ‖c‖ₑ * eLpNorm f p μ

Proof state:
case inr
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup F
𝕜 : Type u_6
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 F
inst✝ : BoundedSMul 𝕜 F
c : 𝕜
f : α → F
p : ℝ≥0∞
μ : Measure α
hc : c ≠ 0
⊢ eLpNorm f p μ ≤ eLpNorm (c • f) p μ / ‖c‖ₑ

Tactic:
simpa [enorm_inv, hc, ENNReal.div_eq_inv_mul]
  using eLpNorm_const_smul_le (c := c⁻¹) (f := c • f)

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem mem_symm_trans_source {e' : PartialEquiv α γ} {x : α} (he : x ∈ e.source)
    (he' : x ∈ e'.source) : e x ∈ (e.symm.trans e').source :=
  ⟨e.mapsTo he, by rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e x ∈ ↑e.symm.symm.symm ⁻¹' e'.source

Tactic:
rwa [mem_preimage, PartialEquiv.symm_symm, e.left_inv he]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x

Proof state:
x y : Nat
⊢ x.gcd y = if x = 0 then y else (y % x).gcd x

Tactic:
cases x <;> simp [Nat.gcd_add_one]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem det_toMatrix_prod [Fintype n] (L : List (TransvectionStruct n 𝕜)) :
    det (L.map toMatrix).prod = 1

Proof state:
case nil
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ (List.map toMatrix []).prod.det = 1

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
L : List (TransvectionStruct n 𝕜)
⊢ (List.map toMatrix L).prod.det = 1

Tactic:
induction L with
| nil => simp
| cons _ _ IH => simp [IH]

Result:
no goals

Proof state:
case cons
n : Type u_1
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : DecidableEq n
inst✝ : Fintype n
head✝ : TransvectionStruct n 𝕜
tail✝ : List (TransvectionStruct n 𝕜)
IH : (List.map toMatrix tail✝).prod.det = 1
⊢ (List.map toMatrix (head✝ :: tail✝)).prod.det = 1

Tactic:
simp [IH]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis'_iff_isBasis (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.IsBasis' I X ↔ M.IsBasis I X

Tactic:
rw [isBasis'_iff_isBasis_inter_ground, inter_eq_self_of_subset_left hX]

Result:
no goals