harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Ring/Seminorm.lean
/-- Equivalence of multiplicative ring norms is symmetric. -/
@[deprecated "Use AbsoluteValue.isEquiv_symm instead" (since := "2025-01-07")]
lemma equiv_symm {f g : MulRingNorm R} (hfg : equiv f g) : equiv g f

Proof state:
case h
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ 0 < 1 / c ∧ (fun x => g x ^ (1 / c)) = ⇑f

Tactic:
constructor

Result:
case h.left
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ 0 < 1 / c

case h.right
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ (fun x => g x ^ (1 / c)) = ⇑f

Proof state:
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
hfg : f.equiv g
⊢ g.equiv f

Tactic:
rcases hfg with ⟨c, hcpos, h⟩

Result:
case intro.intro
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ g.equiv f

Proof state:
case intro.intro
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ g.equiv f

Tactic:
use 1/c

Result:
case h
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ 0 < 1 / c ∧ (fun x => g x ^ (1 / c)) = ⇑f

Proof state:
case h.right.h
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
x : R
⊢ g x ^ (1 / c) = f x

Tactic:
simpa [← congr_fun h x] using Real.rpow_rpow_inv (apply_nonneg f x) (ne_of_lt hcpos).symm

Result:
no goals

Proof state:
case h.left
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ 0 < 1 / c

Tactic:
simp only [one_div, inv_pos, hcpos]

Result:
no goals

Proof state:
case h.right
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
⊢ (fun x => g x ^ (1 / c)) = ⇑f

Tactic:
ext x

Result:
case h.right.h
R : Type u_2
inst✝ : Ring R
f g : MulRingNorm R
c : ℝ
hcpos : 0 < c
h : (fun x => f x ^ c) = ⇑g
x : R
⊢ g x ^ (1 / c) = f x
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem sInter_polar_eq_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {r : ℝ} (hr : 0 < r) :
    ⋂₀ (polar 𝕜 '' { F | F.Finite ∧ F ⊆ closedBall (0 : E) r⁻¹ }) = closedBall 0 r

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ ⋂₀ (polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}) = closedBall 0 r⁻¹⁻¹

Tactic:
rw [← polar_closedBall (inv_pos_of_pos hr), polar,
  (dualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]

Result:
no goals

Proof state:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ ⋂₀ (polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}) = closedBall 0 r

Tactic:
conv_rhs => rw [← inv_inv r]

Result:
𝕜 : Type u_3
E : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
hr : 0 < r
⊢ ⋂₀ (polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall 0 r⁻¹}) = closedBall 0 r⁻¹⁻¹
-- Mathlib/Algebra/Colimit/Finiteness.lean
lemma equiv_comp_of (N : {N : Submodule R M // N.FG}) :
    (equiv R M).toLinearMap ∘ₗ of _ _ _ _ N = N.1.subtype

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq (Submodule R M)
N : { N // N.FG }
⊢ ↑(equiv R M) ∘ₗ of R { N // N.FG } (fun i => ↥↑i) (fgSystem R M) N = (↑N).subtype

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq (Submodule R M)
N : { N // N.FG }
x✝ : ↥↑N
⊢ (↑(equiv R M) ∘ₗ of R { N // N.FG } (fun i => ↥↑i) (fgSystem R M) N) x✝ = (↑N).subtype x✝

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq (Submodule R M)
N : { N // N.FG }
x✝ : ↥↑N
⊢ (↑(equiv R M) ∘ₗ of R { N // N.FG } (fun i => ↥↑i) (fgSystem R M) N) x✝ = (↑N).subtype x✝

Tactic:
simp [equiv]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Fold.lean
theorem foldl_mul (f : M →ₗ[R] N →ₗ[R] N) (hf) (n : N) (a b : CliffordAlgebra Q) :
    foldl Q f hf n (a * b) = foldl Q f hf (foldl Q f hf n a) b

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x
n : N
a b : CliffordAlgebra Q
⊢ ((foldl Q f hf) n) (a * b) = ((foldl Q f hf) (((foldl Q f hf) n) a)) b

Tactic:
rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem flatMapM_cons [Monad m] [LawfulMonad m] (f : α → m (List β)) :
    (a :: l).flatMapM f = do
      let bs ← f a
      return (bs ++ (← l.flatMapM f))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
⊢ (do
      let bs' ← f a
      flatMapM.loop f l [bs']) =
    do
    let bs ← f a
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Tactic:
congr

Result:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
⊢ (fun bs' => flatMapM.loop f l [bs']) = fun bs => do
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
⊢ flatMapM f (a :: l) = do
    let bs ← f a
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Tactic:
conv => lhs; unfold flatMapM; unfold flatMapM.loop

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
⊢ (do
      let bs' ← f a
      flatMapM.loop f l [bs']) =
    do
    let bs ← f a
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Proof state:
case e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
⊢ (fun bs' => flatMapM.loop f l [bs']) = fun bs => do
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Tactic:
funext bs

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
bs : List β
⊢ flatMapM.loop f l [bs] = do
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
bs : List β
⊢ (fun x => [bs].reverse.flatten ++ x) <$> flatMapM.loop f l [] = do
    let __do_lift ← flatMapM.loop f l []
    pure (bs ++ __do_lift)

Tactic:
simp

Result:
no goals

Proof state:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
bs : List β
⊢ flatMapM.loop f l [bs] = do
    let __do_lift ← flatMapM f l
    pure (bs ++ __do_lift)

Tactic:
rw [flatMapM_loop_eq, flatMapM]

Result:
case e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m (List β)
bs : List β
⊢ (fun x => [bs].reverse.flatten ++ x) <$> flatMapM.loop f l [] = do
    let __do_lift ← flatMapM.loop f l []
    pure (bs ++ __do_lift)
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_toFinset [DecidableEq α] (l : List α) (f : α → β) (comm) (hl : l.Nodup) :
    noncommProd l.toFinset f comm = (l.map f).prod

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
simp [noncommProd, hl]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.Nodup
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
rw [← List.dedup_eq_self] at hl

Result:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod
-- Mathlib/NumberTheory/ZetaValues.lean
theorem antideriv_bernoulliFun (k : ℕ) (x : ℝ) :
    HasDerivAt (fun x => bernoulliFun (k + 1) x / (k + 1)) (bernoulliFun k x) x

Proof state:
case h.e'_9
k : ℕ
x : ℝ
⊢ bernoulliFun k x = ↑(k + 1) * bernoulliFun (k + 1 - 1) x / (↑k + 1)

Tactic:
field_simp [Nat.cast_add_one_ne_zero k]

Result:
no goals

Proof state:
k : ℕ
x : ℝ
⊢ HasDerivAt (fun x => bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x

Tactic:
convert (hasDerivAt_bernoulliFun (k + 1) x).div_const _ using 1

Result:
case h.e'_9
k : ℕ
x : ℝ
⊢ bernoulliFun k x = ↑(k + 1) * bernoulliFun (k + 1 - 1) x / (↑k + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem false_cons_zero : cons false 0#w = 0#(w + 1)

Proof state:
w : Nat
⊢ cons false 0#w = 0#(w + 1)

Tactic:
ext

Result:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ (cons false 0#w).getLsbD i✝ = (0#(w + 1)).getLsbD i✝

Proof state:
case pred
w i✝ : Nat
a✝ : i✝ < w + 1
⊢ (cons false 0#w).getLsbD i✝ = (0#(w + 1)).getLsbD i✝

Tactic:
simp [getLsbD_cons]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem get_eq_iff_eq_coe {a : PartENat} {ha : a.Dom} {b : ℕ} : a.get ha = b ↔ a = b

Proof state:
a : PartENat
ha : a.Dom
b : ℕ
⊢ a.get ha = b ↔ a = ↑b

Tactic:
rw [get_eq_iff_eq_some]

Result:
a : PartENat
ha : a.Dom
b : ℕ
⊢ a = ↑b ↔ a = ↑b

Proof state:
a : PartENat
ha : a.Dom
b : ℕ
⊢ a = ↑b ↔ a = ↑b

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/FreeMonoid/Count.lean
@[to_additive]
lemma countP'_mul (l₁ l₂ : FreeMonoid α) : (l₁ * l₂).countP' p = l₁.countP' p + l₂.countP' p

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ List.countP (fun b => decide (p b)) (toList l₁ ++ toList l₂) =
    List.countP (fun b => decide (p b)) (toList l₁) + List.countP (fun b => decide (p b)) (toList l₂)

Tactic:
simp only [List.countP_append]

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ countP' p (l₁ * l₂) = countP' p l₁ + countP' p l₂

Tactic:
dsimp [countP']

Result:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ List.countP (fun b => decide (p b)) (toList l₁ ++ toList l₂) =
    List.countP (fun b => decide (p b)) (toList l₁) + List.countP (fun b => decide (p b)) (toList l₂)
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
@[simp]
lemma scaleRoots_mul (p : R[X]) (r s) :
    p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s

Proof state:
case a
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r s : R
n✝ : ℕ
⊢ (p.scaleRoots (r * s)).coeff n✝ = ((p.scaleRoots r).scaleRoots s).coeff n✝

Tactic:
simp [mul_pow, mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r s : R
⊢ p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : CommSemiring R
p : R[X]
r s : R
n✝ : ℕ
⊢ (p.scaleRoots (r * s)).coeff n✝ = ((p.scaleRoots r).scaleRoots s).coeff n✝
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma empty_nmem_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    ∅ ∉ hC.disjointOfDiff hs ht

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ∅ ∉ hC.disjointOfDiff hs ht

Tactic:
simp only [disjointOfDiff, mem_sdiff, Finset.mem_singleton, eq_self_iff_true,
  not_true, and_false, not_false_iff]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ∅ ∉ hC.disjointOfDiff hs ht

Tactic:
classical
simp only [disjointOfDiff, mem_sdiff, Finset.mem_singleton, eq_self_iff_true,
  not_true, and_false, not_false_iff]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem norm_toLp_le_seminorm (p : ℝ≥0∞) (μ : Measure E

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ eLpNorm (⇑f) p μ ≤ ENNReal.ofReal (↑C * ((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)

Tactic:
rw [ENNReal.ofReal_mul NNReal.zero_le_coe]

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : OpensMeasurableSpace E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 F
inst✝¹ : SMulCommClass ℝ 𝕜 F
inst✝ : SecondCountableTopologyEither E F
p : ℝ≥0∞
μ : autoParam (Measure E) _auto✝
hμ : Measure.HasTemperateGrowth μ
k : ℕ
C : ℝ≥0
hC :
  ∀ (f : 𝓢(E, F)), eLpNorm (⇑f) p μ ≤ ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
f : 𝓢(E, F)
⊢ eLpNorm (⇑f) p μ ≤ ENNReal.ofReal ↑C * ENNReal.ofReal (((Finset.Iic (k, 0)).sup (schwartzSeminormFamily 𝕜 E F)) f)
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
lemma linearIndependent_aeval_val_pderiv_relation :
    LinearIndependent S (fun i j ↦ (aeval P.val) (pderiv (P.map j) (P.relation i)))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ LinearIndependent S fun i j => P.basisDeriv i j

Tactic:
exact P.basisDeriv.linearIndependent

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ LinearIndependent S fun i j => (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
simp_rw [← SubmersivePresentation.basisDeriv_apply]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
⊢ LinearIndependent S fun i j => P.basisDeriv i j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : Vector α n) (init : β) :
    (l.filter p).foldlM g init =
      l.foldlM (fun x y => if p y then g x y else pure x) init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
l : Vector α n
init : β
⊢ Array.foldlM g init (Array.filter p l.toArray) = foldlM (fun x y => if p y = true then g x y else pure x) init l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
init : β
l : Array α
⊢ Array.foldlM g init (Array.filter p { toArray := l, size_toArray := ⋯ }.toArray) =
    foldlM (fun x y => if p y = true then g x y else pure x) init { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
init : β
l : Array α
⊢ Array.foldlM g init (Array.filter p { toArray := l, size_toArray := ⋯ }.toArray) =
    foldlM (fun x y => if p y = true then g x y else pure x) init { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldlM_filter]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Cardinal.lean
theorem rankFinite_iff_cRank_lt_aleph0 : M.RankFinite ↔ M.cRank < ℵ₀

Proof state:
α : Type u
M : Matroid α
⊢ M.RankFinite ↔ M.cRank < ℵ₀

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨?_⟩⟩

Result:
case refine_1
α : Type u
M : Matroid α
h : M.RankFinite
⊢ M.cRank < ℵ₀

case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
⊢ ∃ B, M.IsBase B ∧ B.Finite

Proof state:
case refine_1
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
fin : B.Finite
⊢ M.cRank < ℵ₀

Tactic:
exact hB.cardinalMk_eq_cRank ▸ lt_aleph0_iff_finite.mpr fin

Result:
no goals

Proof state:
case refine_1
α : Type u
M : Matroid α
h : M.RankFinite
⊢ M.cRank < ℵ₀

Tactic:
have ⟨B, hB, fin⟩ := h

Result:
case refine_1
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
fin : B.Finite
⊢ M.cRank < ℵ₀

Proof state:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ #↑B < ℵ₀

Tactic:
exact ⟨B, hB, hB.cardinalMk_le_cRank.trans_lt h⟩

Result:
no goals

Proof state:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B.Finite

Tactic:
simp_rw [← finite_coe_iff, ← lt_aleph0_iff_finite]

Result:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ #↑B < ℵ₀

Proof state:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
⊢ ∃ B, M.IsBase B ∧ B.Finite

Tactic:
have ⟨B, hB⟩ := M.exists_isBase

Result:
case refine_2
α : Type u
M : Matroid α
h : M.cRank < ℵ₀
B : Set α
hB : M.IsBase B
⊢ ∃ B, M.IsBase B ∧ B.Finite
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem t_snd (i j : 𝒰.J) : t 𝒰 f g i j ≫ pullback.snd _ _ =
    pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i j : 𝒰.J
⊢ t 𝒰 f g i j ≫ pullback.snd (pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) =
    pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ pullback.fst (𝒰.map i ≫ f) g

Tactic:
simp only [t, Category.assoc, pullbackSymmetry_hom_comp_snd, pullbackAssoc_hom_fst,
  pullback.lift_fst_assoc, pullbackSymmetry_hom_comp_fst, pullbackAssoc_inv_fst_snd,
  pullbackSymmetry_hom_comp_snd_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem pullback_id : S.pullback (𝟙 _) = S

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
⊢ pullback (𝟙 X) S = S

Tactic:
simp [Sieve.ext_iff]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_comp_left {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) :
    k (eval₂ f g p) = eval₂ (k.comp f) (k ∘ g) p

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ k (eval₂ f g p) = eval₂ (k.comp f) (⇑k ∘ g) p

Tactic:
apply MvPolynomial.induction_on p <;>
  simp +contextual [eval₂_add, k.map_add, eval₂_mul, k.map_mul]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldr_eq_of_comm' (hf : ∀ a b c, f a (f b c) = f b (f a c)) :
    ∀ a b l, foldr f a (b :: l) = foldr f (f b a) l
  | _, _, [] => rfl
  | a, b, c :: l => by rw [foldr, foldr, foldr, hf, ← foldr_eq_of_comm' hf ..]; rfl

Proof state:
α : Type u
β : Type v
f : α → β → β
hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)
a : β
b c : α
l : List α
⊢ f c (f b (foldr f a l)) = f c (foldr f a (b :: l))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β → β
hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)
a : β
b c : α
l : List α
⊢ foldr f a (b :: c :: l) = foldr f (f b a) (c :: l)

Tactic:
rw [foldr, foldr, foldr, hf, ← foldr_eq_of_comm' hf ..]

Result:
α : Type u
β : Type v
f : α → β → β
hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)
a : β
b c : α
l : List α
⊢ f c (f b (foldr f a l)) = f c (foldr f a (b :: l))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ofNat_fmod (m n : Nat) : ↑(m % n) = fmod m n

Proof state:
m n : Nat
⊢ ↑(m % n) = (↑m).fmod ↑n

Tactic:
cases m <;> simp [fmod, Nat.succ_eq_add_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernelZeroIsoSource_inv :
    kernelZeroIsoSource.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ kernelZeroIsoSource.inv = kernel.lift 0 (𝟙 X) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ kernelZeroIsoSource.inv ≫ equalizer.ι 0 0 = kernel.lift 0 (𝟙 X) ⋯ ≫ equalizer.ι 0 0

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
⊢ kernelZeroIsoSource.inv ≫ equalizer.ι 0 0 = kernel.lift 0 (𝟙 X) ⋯ ≫ equalizer.ι 0 0

Tactic:
simp [kernelZeroIsoSource]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ 𝟙 X ≫ 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem nndist_eq_zero {x y : γ} : nndist x y = 0 ↔ x = y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ nndist x y = 0 ↔ x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, dist_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
lemma iSup_ringCon {ι : Type*} (I : ι → TwoSidedIdeal R) :
    (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon

Proof state:
case e_a
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i => I i) = Set.range fun i => (I i).ringCon

Tactic:
ext

Result:
case e_a.h
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i => I i) ↔ x✝ ∈ Set.range fun i => (I i).ringCon

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sSup (ringCon '' Set.range fun i => I i) = sSup (Set.range fun i => (I i).ringCon)

Tactic:
congr

Result:
case e_a
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i => I i) = Set.range fun i => (I i).ringCon

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (⨆ i, I i).ringCon = ⨆ i, (I i).ringCon

Tactic:
simp only [iSup, sSup_ringCon]

Result:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sSup (ringCon '' Set.range fun i => I i) = sSup (Set.range fun i => (I i).ringCon)

Proof state:
case e_a.h
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i => I i) ↔ x✝ ∈ Set.range fun i => (I i).ringCon

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_add : ∀ a b, (a + b : ℝ).cauchy = a.cauchy + b.cauchy
  | ⟨a⟩, ⟨b⟩ => show (add _ _).cauchy = _ by rw [add_def]

Proof state:
a b : Cauchy abs
⊢ (Real.add { cauchy := a } { cauchy := b }).cauchy = { cauchy := a }.cauchy + { cauchy := b }.cauchy

Tactic:
rw [add_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem mul_nonsing_inv (h : IsUnit A.det) : A * A⁻¹ = 1

Proof state:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A * A⁻¹ = 1

Tactic:
rw [← invOf_eq_nonsing_inv, mul_invOf_self]

Result:
no goals

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
⊢ A * A⁻¹ = 1

Tactic:
cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible

Result:
case intro
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : IsUnit A.det
val✝ : Invertible A
⊢ A * A⁻¹ = 1