harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FiniteType.lean
theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M}
    (hS : closure S = ⊤) :
    Function.Surjective
      (FreeAlgebra.lift R fun s : S => of' R M ↑s : FreeAlgebra R S → R[M])

Proof state:
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = g
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = ((FreeAlgebra.lift R) fun s => of' R M ↑s) P + g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Result:
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s => of' R M ↑s) a =
      ((FreeAlgebra.lift R) fun s => of' R M ↑s) P + ((FreeAlgebra.lift R) fun s => of' R M ↑s) Q

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : R[M]
ihf : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = g
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f + g

Tactic:
rcases ihf with ⟨P, rfl⟩

Result:
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : R[M]
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = g
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = ((FreeAlgebra.lift R) fun s => of' R M ↑s) P + g

Proof state:
case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = r • f

Tactic:
rcases ih with ⟨P, rfl⟩

Result:
case hsmul.intro
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = r • ((FreeAlgebra.lift R) fun s => of' R M ↑s) P

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f

Tactic:
induction' f using induction_on with m f g ihf ihg r f ih

Result:
case hM
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)

case hadd
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f g : R[M]
ihf : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = g
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f + g

case hsmul
R : Type u_1
M : Type u_2
inst✝¹ : AddMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
r : R
f : R[M]
ih : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = r • f
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformSpace_comap_id {α : Type*} : UniformSpace.comap (id : α → α) = id

Proof state:
case h.h
α : Type u_2
x✝ : UniformSpace α
⊢ 𝓤 α = 𝓤 α

Tactic:
rw [uniformity_comap, Prod.map_id, comap_id]

Result:
no goals

Proof state:
α : Type u_2
⊢ UniformSpace.comap id = id

Tactic:
ext : 2

Result:
case h.h
α : Type u_2
x✝ : UniformSpace α
⊢ 𝓤 α = 𝓤 α
-- Mathlib/Topology/FiberBundle/IsHomeomorphicTrivialBundle.lean
theorem isOpenMap_proj (h : IsHomeomorphicTrivialFiberBundle F proj) :
    IsOpenMap proj

Proof state:
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ IsOpenMap (Prod.fst ∘ ⇑e)

Tactic:
exact isOpenMap_fst.comp e.isOpenMap

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ IsOpenMap proj

Tactic:
obtain ⟨e, rfl⟩ := h.proj_eq

Result:
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ IsOpenMap (Prod.fst ∘ ⇑e)
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟ A = ⅟ A.det • A.adjugate

Proof state:
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A.det
inst✝ : Invertible A
⊢ ⅟A = ⅟A.det • A.adjugate

Tactic:
letI := invertibleOfDetInvertible A

Result:
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A.det
inst✝ : Invertible A
this : Invertible A := A.invertibleOfDetInvertible
⊢ ⅟A = ⅟A.det • A.adjugate

Proof state:
n : Type u'
α : Type v
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing α
A : Matrix n n α
inst✝¹ : Invertible A.det
inst✝ : Invertible A
this : Invertible A := A.invertibleOfDetInvertible
⊢ ⅟A = ⅟A.det • A.adjugate

Tactic:
convert (rfl : ⅟ A = _)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/PeakFunction.lean
theorem tendsto_integral_comp_smul_smul_of_integrable'
    {φ : F → ℝ} (hφ : ∀ x, 0 ≤ φ x) (h'φ : ∫ x, φ x ∂μ = 1)
    (h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0))
    {g : F → E} {x₀ : F} (hg : Integrable g μ) (h'g : ContinuousAt g x₀) :
    Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • (x₀ - x))) • g x ∂μ)
      atTop (𝓝 (g x₀))

Proof state:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))

Tactic:
simp only [f, sub_zero] at this

Result:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : FiniteDimensional ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure F
inst✝ : μ.IsAddHaarMeasure
φ : F → ℝ
hφ : ∀ (x : F), 0 ≤ φ x
h'φ : ∫ (x : F), φ x ∂μ = 1
h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)
g : F → E
x₀ : F
hg : Integrable g μ
h'g : ContinuousAt g x₀
f : F → E := fun x => g (x₀ - x)
If : Integrable f μ
this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))
⊢ Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
-- Mathlib/Algebra/Polynomial/Div.lean
/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree` for the general case. -/
lemma rootMultiplicity_eq_natTrailingDegree' : p.rootMultiplicity 0 = p.natTrailingDegree

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
by_cases h : p = 0

Result:
case pos
R : Type u
inst✝ : CommRing R
p : R[X]
h : p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

case neg
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Proof state:
case neg
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
refine le_antisymm ?_ ?_

Result:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Proof state:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0

Tactic:
exact fun _ ↦ coeff_eq_zero_of_lt_natTrailingDegree

Result:
no goals

Proof state:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ x, ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)

Tactic:
exact ⟨p.natTrailingDegree,
  fun h' ↦ trailingCoeff_nonzero_iff_nonzero.2 h <| h' <| Nat.lt.base _⟩

Result:
no goals

Proof state:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ p.natTrailingDegree ≤ rootMultiplicity 0 p

Tactic:
rw [le_rootMultiplicity_iff h, map_zero, sub_zero, X_pow_dvd_iff]

Result:
case neg.refine_2
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∀ d < p.natTrailingDegree, p.coeff d = 0

Proof state:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ rootMultiplicity 0 p ≤ p.natTrailingDegree

Tactic:
rw [rootMultiplicity_le_iff h, map_zero, sub_zero, X_pow_dvd_iff, not_forall]

Result:
case neg.refine_1
R : Type u
inst✝ : CommRing R
p : R[X]
h : ¬p = 0
⊢ ∃ x, ¬(x < p.natTrailingDegree + 1 → p.coeff x = 0)

Proof state:
case pos
R : Type u
inst✝ : CommRing R
p : R[X]
h : p = 0
⊢ rootMultiplicity 0 p = p.natTrailingDegree

Tactic:
simp only [h, rootMultiplicity_zero, natTrailingDegree_zero]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem _root_.IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible {K : Type*} [Field K]
    {R : Type*} [CommRing R] [IsDomain R] {μ : R} {n : ℕ} [Algebra K R] (hμ : IsPrimitiveRoot μ n)
    (h : Irreducible <| cyclotomic n K) [NeZero (n : K)] : cyclotomic n K = minpoly K μ

Proof state:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ

Tactic:
refine minpoly.eq_of_irreducible_of_monic h ?_ (cyclotomic.monic n K)

Result:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ (aeval μ) (cyclotomic n K) = 0

Proof state:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ (aeval μ) (cyclotomic n K) = 0

Tactic:
rwa [aeval_def, eval₂_eq_eval_map, map_cyclotomic, ← IsRoot.def, isRoot_cyclotomic_iff]

Result:
no goals

Proof state:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ

Tactic:
haveI := NeZero.of_faithfulSMul K R n

Result:
K : Type u_2
inst✝⁴ : Field K
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDomain R
μ : R
n : ℕ
inst✝¹ : Algebra K R
hμ : IsPrimitiveRoot μ n
h : Irreducible (cyclotomic n K)
inst✝ : NeZero ↑n
this : NeZero ↑n
⊢ cyclotomic n K = minpoly K μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_two_pow {n m : Nat} : testBit (2 ^ n) m = decide (n = m)

Proof state:
n m : Nat
h : ¬n = m
h✝ : n < m
⊢ 1 < 2

Tactic:
omega

Result:
no goals

Proof state:
case neg
n m : Nat
h : ¬n = m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide (n = m)

Tactic:
simp only [h]

Result:
case neg
n m : Nat
h : ¬n = m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide False

Proof state:
case neg.inr
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide False

Tactic:
rw [Nat.pow_div _ Nat.two_pos,
   ← Nat.sub_add_cancel (succ_le_of_lt <| Nat.sub_pos_of_lt (by omega))]

Result:
case neg.inr
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ (1 &&& 2 ^ (n - m - succ 0 + succ 0) != 0) = decide False

n m : Nat
h : ¬n = m
h✝ : m < n
⊢ m ≤ n

Proof state:
case neg
n m : Nat
h : ¬n = m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide False

Tactic:
cases Nat.lt_or_lt_of_ne h

Result:
case neg.inl
n m : Nat
h : ¬n = m
h✝ : n < m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide False

case neg.inr
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide False

Proof state:
case pos
n m : Nat
h : n = m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide (n = m)

Tactic:
simp [h, Nat.div_self (Nat.pow_pos Nat.zero_lt_two)]

Result:
no goals

Proof state:
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ m < n

Tactic:
omega

Result:
no goals

Proof state:
n m : Nat
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide (n = m)

Tactic:
by_cases h : n = m

Result:
case pos
n m : Nat
h : n = m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide (n = m)

case neg
n m : Nat
h : ¬n = m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide (n = m)

Proof state:
n m : Nat
⊢ (2 ^ n).testBit m = decide (n = m)

Tactic:
rw [testBit, shiftRight_eq_div_pow]

Result:
n m : Nat
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide (n = m)

Proof state:
case neg.inl
n m : Nat
h : ¬n = m
h✝ : n < m
⊢ (1 &&& 2 ^ n / 2 ^ m != 0) = decide False

Tactic:
rw [div_eq_of_lt (Nat.pow_lt_pow_of_lt (by omega) (by omega))]

Result:
case neg.inl
n m : Nat
h : ¬n = m
h✝ : n < m
⊢ (1 &&& 0 != 0) = decide False

Proof state:
case neg.inr
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ (1 &&& 2 ^ (n - m - succ 0 + succ 0) != 0) = decide False

n m : Nat
h : ¬n = m
h✝ : m < n
⊢ m ≤ n

Tactic:
simp [Nat.pow_succ, and_one_is_mod, mul_mod_left]

Result:
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ m ≤ n

Proof state:
n m : Nat
h : ¬n = m
h✝ : n < m
⊢ n < m

Tactic:
omega

Result:
no goals

Proof state:
case neg.inl
n m : Nat
h : ¬n = m
h✝ : n < m
⊢ (1 &&& 0 != 0) = decide False

Tactic:
simp

Result:
no goals

Proof state:
n m : Nat
h : ¬n = m
h✝ : m < n
⊢ m ≤ n

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem zipWith_single_single (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N) :
    zipWith f hf (single a m) (single a n) = single a (f m n)

Proof state:
case h.inr
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
a' : α
ha' : a ≠ a'
⊢ f ((single a m) a') ((single a n) a') = (single a (f m n)) a'

Tactic:
rw [single_eq_of_ne ha', single_eq_of_ne ha', single_eq_of_ne ha', hf]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
a' : α
⊢ (zipWith f hf (single a m) (single a n)) a' = (single a (f m n)) a'

Tactic:
rw [zipWith_apply]

Result:
case h
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
a' : α
⊢ f ((single a m) a') ((single a n) a') = (single a (f m n)) a'

Proof state:
case h.inl
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ f ((single a m) a) ((single a n) a) = (single a (f m n)) a

Tactic:
rw [single_eq_same, single_eq_same, single_eq_same]

Result:
no goals

Proof state:
case h
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
a' : α
⊢ f ((single a m) a') ((single a n) a') = (single a (f m n)) a'

Tactic:
obtain rfl | ha' := eq_or_ne a a'

Result:
case h.inl
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ f ((single a m) a) ((single a n) a) = (single a (f m n)) a

case h.inr
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
a' : α
ha' : a ≠ a'
⊢ f ((single a m) a') ((single a n) a') = (single a (f m n)) a'

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
⊢ zipWith f hf (single a m) (single a n) = single a (f m n)

Tactic:
ext a'

Result:
case h
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M → N → P
hf : f 0 0 = 0
a : α
m : M
n : N
a' : α
⊢ (zipWith f hf (single a m) (single a n)) a' = (single a (f m n)) a'
-- Mathlib/Topology/Basic.lean
theorem closure_diff : closure s \ closure t ⊆ closure (s \ t) :=
  calc
    closure s \ closure t = (closure t)ᶜ ∩ closure s

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
⊢ closure s \ closure t = (closure t)ᶜ ∩ closure s

Tactic:
simp only [diff_eq, inter_comm]

Result:
no goals

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
⊢ closure ((closure t)ᶜ ∩ s) = closure (s \ closure t)

Tactic:
simp only [diff_eq, inter_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/DiagramLemmas/KernelCokernelComp.lean
lemma δ_fac : δ f g = - kernel.ι g ≫ cokernel.π f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ δ f g = -kernel.ι g ≫ cokernel.π f

Tactic:
simpa using (snakeInput f g).δ_eq (𝟙 _) (kernel.ι g ≫ biprod.inr) (-kernel.ι g)
  (by simp) (by aesop)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (kernel.ι g ≫ biprod.inr) ≫ (snakeInput f g).L₁.g = 𝟙 (snakeInput f g).L₀.X₃ ≫ (snakeInput f g).v₀₁.τ₃

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (-kernel.ι g) ≫ (snakeInput f g).L₂.f = (kernel.ι g ≫ biprod.inr) ≫ (snakeInput f g).v₁₂.τ₂

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.equiv_symm {v : Basis ι 𝕜 E} (hv : Orthonormal 𝕜 v) {v' : Basis ι' 𝕜 E'}
    (hv' : Orthonormal 𝕜 v') (e : ι ≃ ι') : (hv.equiv hv' e).symm = hv'.equiv hv e.symm :=
  v'.ext_linearIsometryEquiv fun i =>
    (hv.equiv hv' e).injective <| by
      simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
E' : Type u_6
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
v : Basis ι 𝕜 E
hv : Orthonormal 𝕜 ⇑v
v' : Basis ι' 𝕜 E'
hv' : Orthonormal 𝕜 ⇑v'
e : ι ≃ ι'
i : ι'
⊢ (hv.equiv hv' e) ((hv.equiv hv' e).symm (v' i)) = (hv.equiv hv' e) ((hv'.equiv hv e.symm) (v' i))

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply, Orthonormal.equiv_apply, e.apply_symm_apply]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_eq_top_iff : krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

Proof state:
case inr.inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
rw [krullDim_eq_length_of_finiteDimensionalOrder] at h

Result:
case inr.inl
α : Type u_1
inst✝ : Preorder α
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
h : ↑(LTSeries.longestOf α).length = ⊤
⊢ InfiniteDimensionalOrder α

Proof state:
case inr.inl
α : Type u_1
inst✝ : Preorder α
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
h : ↑(LTSeries.longestOf α).length = ⊤
⊢ InfiniteDimensionalOrder α

Tactic:
cases h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
⊢ InfiniteDimensionalOrder α

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : IsEmpty α
⊢ InfiniteDimensionalOrder α

case inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : Nonempty α
⊢ InfiniteDimensionalOrder α

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α = ⊤ ↔ InfiniteDimensionalOrder α

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

Result:
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
⊢ InfiniteDimensionalOrder α

Proof state:
case inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : Nonempty α
⊢ InfiniteDimensionalOrder α

Tactic:
cases finiteDimensionalOrder_or_infiniteDimensionalOrder α

Result:
case inr.inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

case inr.inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Proof state:
case inl
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝ : IsEmpty α
⊢ InfiniteDimensionalOrder α

Tactic:
simp [krullDim_eq_bot] at h

Result:
no goals

Proof state:
case inr.inr
α : Type u_1
inst✝ : Preorder α
h : krullDim α = ⊤
h✝¹ : Nonempty α
h✝ : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder α

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Regular/SMul.lean
theorem subsingleton (h : IsSMulRegular M (0 : R)) : Subsingleton M :=
  ⟨fun a b => h (by dsimp only [Function.comp_def]; repeat' rw [MulActionWithZero.zero_smul])⟩

Proof state:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ (fun x => 0 • x) a = (fun x => 0 • x) b

Tactic:
dsimp only [Function.comp_def]

Result:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b

Proof state:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b

Tactic:
rw [MulActionWithZero.zero_smul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b

Tactic:
repeat' rw [MulActionWithZero.zero_smul]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma map_dual {hf} : (M.map f hf)✶ = M✶.map f hf

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B

Tactic:
exact fun _ ↦ ⟨B, hB, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶.E = (M✶.map f hf).E

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.IsBase B ↔ (M✶.map f hf).IsBase B)

Tactic:
simp only [dual_ground, map_ground, subset_image_iff, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂, dual_isBase_iff']

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ ∀ a ⊆ M.E, ((M.map f hf).IsBase (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).IsBase (f '' a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ (M.map f hf)✶ = M✶.map f hf

Tactic:
apply ext_isBase (by simp)

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ ∀ ⦃B : Set β⦄, B ⊆ (M.map f hf)✶.E → ((M.map f hf)✶.IsBase B ↔ (M✶.map f hf).IsBase B)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)

Tactic:
simp_rw [← hf.image_diff_subset hB, map_image_isBase_iff diff_subset,
  map_image_isBase_iff (show B ⊆ M✶.E from hB), dual_isBase_iff hB, and_iff_left_iff_imp]

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase (M.E \ B) → ∃ u ⊆ M.E, f '' u = f '' B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
⊢ ∀ a ⊆ M.E, ((M.map f hf).IsBase (f '' M.E \ f '' a) ∧ ∃ u ⊆ M.E, f '' u = f '' a) ↔ (M✶.map f hf).IsBase (f '' a)

Tactic:
intro B hB

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)