harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem exists_ideal_over_maximal_of_isIntegral [Algebra.IsIntegral R S]
    (P : Ideal R) [P_max : IsMaximal P] (hP : RingHom.ker (algebraMap R S) ≤ P) :
    ∃ Q : Ideal S, IsMaximal Q ∧ Q.comap (algebraMap R S) = P

Proof state:
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
P : Ideal R
P_max : P.IsMaximal
hP : RingHom.ker (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : Q.IsPrime
hQ : comap (algebraMap R S) Q = P
⊢ ∃ Q, Q.IsMaximal ∧ comap (algebraMap R S) Q = P

Tactic:
exact ⟨Q, isMaximal_of_isIntegral_of_isMaximal_comap _ (hQ.symm ▸ P_max), hQ⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
P : Ideal R
P_max : P.IsMaximal
hP : RingHom.ker (algebraMap R S) ≤ P
⊢ ∃ Q, Q.IsMaximal ∧ comap (algebraMap R S) Q = P

Tactic:
obtain ⟨Q, -, Q_prime, hQ⟩ := exists_ideal_over_prime_of_isIntegral P ⊥ hP

Result:
case intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
P : Ideal R
P_max : P.IsMaximal
hP : RingHom.ker (algebraMap R S) ≤ P
Q : Ideal S
Q_prime : Q.IsPrime
hQ : comap (algebraMap R S) Q = P
⊢ ∃ Q, Q.IsMaximal ∧ comap (algebraMap R S) Q = P
-- Mathlib/Data/Complex/Trigonometric.lean
theorem two_mul_cos_mul_cos (x y : ℝ) : 2 * cos x * cos y = cos (x - y) + cos (x + y)

Proof state:
x y : ℝ
⊢ 2 * cos x * cos y = cos (x - y) + cos (x + y)

Tactic:
simp [cos_add, cos_sub]

Result:
x y : ℝ
⊢ 2 * cos x * cos y = cos x * cos y + cos x * cos y

Proof state:
x y : ℝ
⊢ 2 * cos x * cos y = cos x * cos y + cos x * cos y

Tactic:
ring

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem fg_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) :
    (Algebra.adjoin R s).toSubmodule.FG :=
  Set.Finite.induction_on _ hfs
    (fun _ =>
      ⟨{1},
        Submodule.ext fun x => by
          rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]⟩)
    (fun {a s} _ _ ih his => by
      rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
      exact
        FG.mul (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
          (his a <| Set.mem_insert a s).fg_adjoin_singleton)
    his

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
hfs : s✝.Finite
his✝ : ∀ x ∈ s✝, IsIntegral R x
a : A
s : Set A
x✝¹ : a ∉ s
x✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R (insert a s))).FG

Tactic:
rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
hfs : s✝.Finite
his✝ : ∀ x ∈ s✝, IsIntegral R x
a : A
s : Set A
x✝¹ : a ∉ s
x✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule (Algebra.adjoin R {a})).FG

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s✝ : Set A
hfs : s✝.Finite
his✝ : ∀ x ∈ s✝, IsIntegral R x
a : A
s : Set A
x✝¹ : a ∉ s
x✝ : s.Finite
ih : (∀ x ∈ s, IsIntegral R x) → (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG
his : ∀ x ∈ insert a s, IsIntegral R x
⊢ (Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule (Algebra.adjoin R {a})).FG

Tactic:
exact
  FG.mul (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
    (his a <| Set.mem_insert a s).fg_adjoin_singleton

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
hfs : s.Finite
his : ∀ x ∈ s, IsIntegral R x
x✝ : ∀ x ∈ ∅, IsIntegral R x
x : A
⊢ x ∈ span R ↑{1} ↔ x ∈ Subalgebra.toSubmodule (Algebra.adjoin R ∅)

Tactic:
rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem imageMonoIsoSource_hom_self [Mono f] : (imageMonoIsoSource f).hom ≫ f = image.ι f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ f = image.ι f

Tactic:
simp only [← imageMonoIsoSource_inv_ι f]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f

Tactic:
rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]

Result:
no goals
-- Mathlib/Tactic/Order/Preprocessing.lean
lemma le_of_not_lt_le {α : Type u} [Preorder α] {x y : α} (h1 : ¬(x < y)) (h2 : x ≤ y) :
    y ≤ x

Proof state:
case inr
α : Type u
inst✝ : Preorder α
x y : α
h2 : x ≤ y
h1 : y ≤ x
⊢ y ≤ x

Tactic:
assumption

Result:
no goals

Proof state:
case inl
α : Type u
inst✝ : Preorder α
x y : α
h2 : x ≤ y
h1 : ¬x ≤ y
⊢ y ≤ x

Tactic:
exact False.elim (h1 h2)

Result:
no goals

Proof state:
α : Type u
inst✝ : Preorder α
x y : α
h1 : ¬x < y
h2 : x ≤ y
⊢ y ≤ x

Tactic:
rw [not_lt_iff_not_le_or_ge] at h1

Result:
α : Type u
inst✝ : Preorder α
x y : α
h1 : ¬x ≤ y ∨ y ≤ x
h2 : x ≤ y
⊢ y ≤ x

Proof state:
α : Type u
inst✝ : Preorder α
x y : α
h1 : ¬x ≤ y ∨ y ≤ x
h2 : x ≤ y
⊢ y ≤ x

Tactic:
rcases h1 with (h1 | h1)

Result:
case inl
α : Type u
inst✝ : Preorder α
x y : α
h2 : x ≤ y
h1 : ¬x ≤ y
⊢ y ≤ x

case inr
α : Type u
inst✝ : Preorder α
x y : α
h2 : x ≤ y
h1 : y ≤ x
⊢ y ≤ x
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem prodMonoidal_leftUnitor_inv_fst (X : C₁ × C₂) :
    ((λ_ X).inv : X ⟶ 𝟙_ _ ⊗ X).1 = (λ_ X.1).inv

Proof state:
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
X : C₁ × C₂
⊢ (λ_ X).inv.1 = (λ_ X.1).inv

Tactic:
cases X

Result:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).inv.1 = (λ_ (fst✝, snd✝).1).inv

Proof state:
case mk
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
fst✝ : C₁
snd✝ : C₂
⊢ (λ_ (fst✝, snd✝)).inv.1 = (λ_ (fst✝, snd✝).1).inv

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_add_two : ∀ n, U R (n + 2) = 2 * X * U R (n + 1) - U R n
  | (k : ℕ) => U.eq_3 R k
  | -(k + 1 : ℕ) => by linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) U.eq_4 R k

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-↑(k + 1) + 2) = 2 * X * U R (-↑(k + 1) + 1) - U R (-↑(k + 1))

Tactic:
linear_combination (norm := (simp [Int.negSucc_eq]; ring_nf)) U.eq_4 R k

Result:
no goals

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-1 + -↑k + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) - 2 * X * U R (-↑k) = 0

Tactic:
ring_nf

Result:
no goals

Proof state:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-↑(k + 1) + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) -
      (2 * X * U R (-↑(k + 1) + 1) - U R (-↑(k + 1)) + U R (Int.negSucc k)) =
    0

Tactic:
simp [Int.negSucc_eq]

Result:
case a.a
R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ U R (-1 + -↑k + 2) + (2 * X * U R (-↑k) - U R (-↑k + 1)) - 2 * X * U R (-↑k) = 0
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean
theorem tendsto_measure_cthickening_of_isClosed {μ : Measure α} {s : Set α}
    (hs : ∃ R > 0, μ (cthickening R s) ≠ ∞) (h's : IsClosed s) :
    Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ s))

Proof state:
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
h's : IsClosed s
⊢ Tendsto (fun r => μ (cthickening r s)) (𝓝 0) (𝓝 (μ s))

Tactic:
convert tendsto_measure_cthickening hs

Result:
case h.e'_5.h.e'_3.h.e'_6
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
h's : IsClosed s
⊢ s = closure s

Proof state:
case h.e'_5.h.e'_3.h.e'_6
α : Type u_1
inst✝² : PseudoEMetricSpace α
inst✝¹ : MeasurableSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ R > 0, μ (cthickening R s) ≠ ⊤
h's : IsClosed s
⊢ s = closure s

Tactic:
exact h's.closure_eq.symm

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- The non-zero non-`s`-factored numbers are `≥ N` when `s` contains all primes less than `N`. -/
lemma factoredNumbers_compl {N : ℕ} {s : Finset ℕ} (h : primesBelow N ≤ s) :
    (factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}

Proof state:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : n ∈ (factoredNumbers s)ᶜ \ {0}
⊢ n ∈ {n | N ≤ n}

Tactic:
simp only [Set.mem_compl_iff, mem_factoredNumbers, Set.mem_diff, ne_eq, not_and, not_forall,
  not_lt, exists_prop, Set.mem_singleton_iff] at hn

Result:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ n ∈ {n | N ≤ n}

Proof state:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p < N
⊢ p ∈ s

Tactic:
exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩

Result:
no goals

Proof state:
case intro.intro
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
this : N ≤ p
⊢ N ≤ n

Tactic:
exact this.trans <| le_of_mem_primeFactorsList hp₁

Result:
no goals

Proof state:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
⊢ (factoredNumbers s)ᶜ \ {0} ⊆ {n | N ≤ n}

Tactic:
intro n hn

Result:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : n ∈ (factoredNumbers s)ᶜ \ {0}
⊢ n ∈ {n | N ≤ n}

Proof state:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ n ∈ {n | N ≤ n}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ N ≤ n

Proof state:
case intro.intro
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
⊢ N ≤ n

Tactic:
have : N ≤ p := by
  contrapose! hp₂
  exact h <| mem_primesBelow.mpr ⟨hp₂, prime_of_mem_primeFactorsList hp₁⟩

Result:
case intro.intro
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
this : N ≤ p
⊢ N ≤ n

Proof state:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
⊢ N ≤ p

Tactic:
contrapose! hp₂

Result:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p < N
⊢ p ∈ s

Proof state:
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
⊢ N ≤ n

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := hn.1 hn.2

Result:
case intro.intro
N : ℕ
s : Finset ℕ
h : N.primesBelow ≤ s
n : ℕ
hn : (¬n = 0 → ∃ x ∈ n.primeFactorsList, x ∉ s) ∧ ¬n = 0
p : ℕ
hp₁ : p ∈ n.primeFactorsList
hp₂ : p ∉ s
⊢ N ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_ite_empty_right {x : α} [Decidable p] {l : Vector α 0} :
    (x ∈ if p then l else #v[]) ↔ p ∧ x ∈ l

Proof state:
α : Type u_1
p : Prop
x : α
inst✝ : Decidable p
l : Vector α 0
⊢ (x ∈ if p then l else { toArray := #[], size_toArray := ⋯ }) ↔ p ∧ x ∈ l

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem beq_refl (a : Nat) : Nat.beq a a = true

Proof state:
case succ
a : Nat
ih : a.beq a = true
⊢ a.beq a = true

Tactic:
simp [ih]

Result:
no goals

Proof state:
a : Nat
⊢ a.beq a = true

Tactic:
induction a with simp [Nat.beq]
| succ a ih => simp [ih]

Result:
no goals
-- Mathlib/Algebra/Ring/Idempotent.lean
lemma of_mul_add (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ IsIdempotentElem b

Proof state:
case left
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a

Tactic:
conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]

Result:
no goals

Proof state:
case right
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ b * b = b

Tactic:
conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ IsIdempotentElem a ∧ IsIdempotentElem b

Tactic:
simp_rw [IsIdempotentElem]

Result:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = b

Proof state:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a ∧ b * b = b

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ a * a = a

case right
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
⊢ b * b = b
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem map_extChartAt_nhds_of_boundaryless [I.Boundaryless] (x : M) :
    map (extChartAt I x) (𝓝 x) = 𝓝 (extChartAt I x x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ map (↑(extChartAt I x)) (𝓝 x) = 𝓝 (↑(extChartAt I x) x)

Tactic:
rw [extChartAt]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ map (↑((chartAt H x).extend I)) (𝓝 x) = 𝓝 (↑((chartAt H x).extend I) x)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝¹ : ChartedSpace H M
inst✝ : I.Boundaryless
x : M
⊢ map (↑((chartAt H x).extend I)) (𝓝 x) = 𝓝 (↑((chartAt H x).extend I) x)

Tactic:
exact map_extend_nhds_of_boundaryless (chartAt H x) (mem_chart_source H x)

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateRow_apply [DecidableEq m] {i' : m} :
    updateRow M i b i' j = if i' = i then b j else M i' j

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
by_cases h : i' = i

Result:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Proof state:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : ¬i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
rw [updateRow_ne h, if_neg h]

Result:
no goals

Proof state:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ M.updateRow i b i' j = if i' = i then b j else M i' j

Tactic:
rw [h, updateRow_self, if_pos rfl]

Result:
no goals
-- Mathlib/CategoryTheory/Linear/LinearFunctor.lean
theorem map_units_smul {X Y : C} (r : Rˣ) (f : X ⟶ Y) : F.map (r • f) = r • F.map f

Proof state:
R : Type u_1
inst✝⁷ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁶ : Category.{u_4, u_2} C
inst✝⁵ : Category.{u_5, u_3} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : CategoryTheory.Linear R C
inst✝¹ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝ : Linear R F
X Y : C
r : Rˣ
f : X ⟶ Y
⊢ F.map (r • f) = r • F.map f

Tactic:
apply map_smul

Result:
no goals
-- Mathlib/Algebra/Ring/Pointwise/Finset.lean
@[simp]
protected lemma neg_smul [DecidableEq α] : -s • t = -(s • t)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ -s • t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

Result:
α : Type u_1
β : Type u_2
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image (fun x => -x) s • t = image (fun x => -x) (s • t)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Ring α
inst✝³ : AddCommGroup β
inst✝² : Module α β
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image (fun x => -x) s • t = image (fun x => -x) (s • t)

Tactic:
exact image₂_image_left_comm neg_smul

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma codomain_eq (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : p.obj b = S

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝ : p.IsHomLift f φ
⊢ p.obj b = S

Tactic:
subst_hom_lift p f φ

Result:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj b✝ = p.obj b✝

Proof state:
case map
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₂} 𝒳
inst✝¹ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a✝ b✝ : 𝒳
φ : a✝ ⟶ b✝
R S : 𝒮
a b : 𝒳
inst✝ : p.IsHomLift (p.map φ) φ
⊢ p.obj b✝ = p.obj b✝

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem exists_measurable_superset_of_trim_eq_zero {m : OuterMeasure α} {s : Set α}
    (h : m.trim s = 0) : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : m.trim s = 0
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0

Tactic:
rcases exists_measurable_superset_eq_trim m s with ⟨t, hst, ht, hm⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : m.trim s = 0
t : Set α
hst : s ⊆ t
ht : MeasurableSet t
hm : m t = m.trim s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
h : m.trim s = 0
t : Set α
hst : s ⊆ t
ht : MeasurableSet t
hm : m t = m.trim s
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = 0

Tactic:
exact ⟨t, hst, ht, h ▸ hm⟩

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_apply_le_norm_cfc (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σ 𝕜 a)
    (hf : ContinuousOn f (σ 𝕜 a)

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

Tactic:
nontriviality A

Result:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
a✝ : Nontrivial A
⊢ x ∈ σ 𝕜 a → ‖f x‖ ≤ ‖cfc f a‖

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

Tactic:
revert hx

Result:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsometricContinuousFunctionalCalculus 𝕜 A p
f : 𝕜 → 𝕜
a : A
x : 𝕜
hf : autoParam (ContinuousOn f (σ 𝕜 a)) _auto✝
ha : autoParam (p a) _auto✝
⊢ x ∈ σ 𝕜 a → ‖f x‖ ≤ ‖cfc f a‖
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem primitiveRoots_one : primitiveRoots 1 R = {(1 : R)}

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 1 R = {1}

Tactic:
refine Finset.eq_singleton_iff_unique_mem.2 ⟨?_, fun x hx ↦ ?_⟩

Result:
case refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R

case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1

Proof state:
case refine_2
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : R
hx : x ∈ primitiveRoots 1 R
⊢ x = 1

Tactic:
rwa [mem_primitiveRoots zero_lt_one, IsPrimitiveRoot.one_right_iff] at hx

Result:
no goals

Proof state:
case refine_1
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ 1 ∈ primitiveRoots 1 R

Tactic:
simp only [IsPrimitiveRoot.one_right_iff, mem_primitiveRoots zero_lt_one]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Basic.lean
lemma hasColimit_iff_small_quot :
    HasColimit F ↔ Small.{u} (Types.Quot (F ⋙ forget))

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ HasColimit (F ⋙ forget)

Tactic:
constructor <;> intro

Result:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit F
⊢ HasColimit (F ⋙ forget)

case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit (F ⋙ forget)
⊢ HasColimit F

Proof state:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit (F ⋙ forget)
⊢ HasColimit F

Tactic:
exact ⟨⟨_, isColimitCoconeOfForget _ (colimit.isColimit _)⟩⟩

Result:
no goals

Proof state:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit F
⊢ HasColimit (F ⋙ forget)

Tactic:
infer_instance

Result:
no goals

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ Small.{u, max u v} (Types.Quot (F ⋙ forget))

Tactic:
rw [← Types.hasColimit_iff_small_quot]

Result:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F ↔ HasColimit (F ⋙ forget)
-- Mathlib/LinearAlgebra/Dual.lean
theorem iSup_dualAnnihilator_le_iInf {ι : Sort*} (U : ι → Submodule R M) :
    ⨆ i : ι, (U i).dualAnnihilator ≤ (⨅ i : ι, U i).dualAnnihilator

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_1
U : ι → Submodule R M
⊢ ⨅ i, U i ≤ ⨅ i, (U i).dualAnnihilator.dualCoannihilator

Tactic:
apply iInf_mono

Result:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_1
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator

Proof state:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_1
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ (U i).dualAnnihilator.dualCoannihilator

Tactic:
exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_1
U : ι → Submodule R M
⊢ ⨆ i, (U i).dualAnnihilator ≤ (⨅ i, U i).dualAnnihilator

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_1
U : ι → Submodule R M
⊢ ⨅ i, U i ≤ ⨅ i, (U i).dualAnnihilator.dualCoannihilator