harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/GroupExtension/Basic.lean
theorem trans {s₁ s₂ s₃ : S.Splitting} (h₁ : S.IsConj s₁ s₂) (h₂ : S.IsConj s₂ s₃) :
    S.IsConj s₁ s₃

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
h₁ : S.IsConj s₁ s₂
h₂ : S.IsConj s₂ s₃
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₁, hn₁⟩ := h₁

Result:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
h₂ : S.IsConj s₂ s₃
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
⊢ S.IsConj s₁ s₃

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g => S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ ⇑s₁ = fun g => S.inl (n₁ * n₂) * s₃ g * (S.inl (n₁ * n₂))⁻¹

Tactic:
simp only [hn₁, hn₂, map_mul]

Result:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g => S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ (fun g => S.inl n₁ * (S.inl n₂ * s₃ g * (S.inl n₂)⁻¹) * (S.inl n₁)⁻¹) = fun g =>
    S.inl n₁ * S.inl n₂ * s₃ g * (S.inl n₁ * S.inl n₂)⁻¹

Proof state:
case intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
h₂ : S.IsConj s₂ s₃
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
⊢ S.IsConj s₁ s₃

Tactic:
obtain ⟨n₂, hn₂⟩ := h₂

Result:
case intro.intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g => S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ S.IsConj s₁ s₃

Proof state:
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g => S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ (fun g => S.inl n₁ * (S.inl n₂ * s₃ g * (S.inl n₂)⁻¹) * (S.inl n₁)⁻¹) = fun g =>
    S.inl n₁ * S.inl n₂ * s₃ g * (S.inl n₁ * S.inl n₂)⁻¹

Tactic:
group

Result:
no goals

Proof state:
case intro.intro
N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
s₁ s₂ s₃ : S.Splitting
n₁ : N
hn₁ : ⇑s₁ = fun g => S.inl n₁ * s₂ g * (S.inl n₁)⁻¹
n₂ : N
hn₂ : ⇑s₂ = fun g => S.inl n₂ * s₃ g * (S.inl n₂)⁻¹
⊢ S.IsConj s₁ s₃

Tactic:
exact ⟨n₁ * n₂, by simp only [hn₁, hn₂, map_mul]; group⟩

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma map_closure_eq {β : Type*} (M : Matroid α) (f : α → β) (hf) (X : Set β) :
    (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Proof state:
case mp.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ x_1, (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x

Tactic:
refine ⟨x, ⟨hxE, fun hI' ↦ ?_⟩, rfl⟩

Result:
case mp.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
⊢ x ∈ I

Proof state:
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis (f ⁻¹' X ∩ M.E)

Result:
case intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
aux : ∀ ⦃I : Set α⦄, M.Indep I → (M.map f hf).closure (f '' I) = f '' M.closure I
I : Set α
hI : M.IsBasis I (f ⁻¹' X ∩ M.E)
⊢ (M.map f hf).closure X = f '' M.closure (f ⁻¹' X)

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
hI' : M.Indep (insert x I)
y : α
hyI : y ∈ I
hfy : y = x
⊢ x ∈ I

Tactic:
rwa [← hfy]

Result:
no goals

Proof state:
case mp
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
e : β
⊢ ((∃ x ∈ M.E, f x = e) ∧ ∀ (x : Set α), M.Indep x → insert e (f '' I) = f '' x → ∃ x ∈ I, f x = e) →
    ∃ x, (x ∈ M.E ∧ (M.Indep (insert x I) → x ∈ I)) ∧ f x = e

Tactic:
rintro ⟨⟨x, hxE, rfl⟩, h2⟩

Result:
case mp.intro.intro.intro
α : Type u_2
β : Type u_3
M : Matroid α
f : α → β
hf : InjOn f M.E
X : Set β
I : Set α
hI : M.Indep I
x : α
hxE : x ∈ M.E
h2 : ∀ (x_1 : Set α), M.Indep x_1 → insert (f x) (f '' I) = f '' x_1 → ∃ x_2 ∈ I, f x_2 = f x
⊢ ∃ x_1, (x_1 ∈ M.E ∧ (M.Indep (insert x_1 I) → x_1 ∈ I)) ∧ f x_1 = f x
-- Mathlib/Data/Real/ConjExponents.lean
protected lemma inv_inv (ha : a ≠ 0) (hb : b ≠ 0) (hab : a + b = 1) :
    a⁻¹.IsConjExponent b⁻¹ :=
  ⟨(one_lt_inv₀ ha.bot_lt).2 <| by rw [← hab]; exact lt_add_of_pos_right _ hb.bot_lt, by
    simpa only [inv_inv] using hab⟩

Proof state:
a b : ℝ≥0
ha : a ≠ 0
hb : b ≠ 0
hab : a + b = 1
⊢ a⁻¹⁻¹ + b⁻¹⁻¹ = 1

Tactic:
simpa only [inv_inv] using hab

Result:
no goals

Proof state:
a b : ℝ≥0
ha : a ≠ 0
hb : b ≠ 0
hab : a + b = 1
⊢ a < a + b

Tactic:
exact lt_add_of_pos_right _ hb.bot_lt

Result:
no goals

Proof state:
a b : ℝ≥0
ha : a ≠ 0
hb : b ≠ 0
hab : a + b = 1
⊢ a < 1

Tactic:
rw [← hab]

Result:
a b : ℝ≥0
ha : a ≠ 0
hb : b ≠ 0
hab : a + b = 1
⊢ a < a + b
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma nnreal_iff_spectralRadius_le [Algebra ℝ A] {a : A} {t : ℝ≥0} (ht : spectralRadius ℝ a ≤ t) :
    SpectrumRestricts a ContinuousMap.realToNNReal ↔
      spectralRadius ℝ (algebraMap ℝ A t - a) ≤ t

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

Tactic:
have : spectrum ℝ a ⊆ Set.Icc (-t) t := by
  intro x hx
  rw [Set.mem_Icc, ← abs_le, ← Real.norm_eq_abs, ← coe_nnnorm, NNReal.coe_le_coe,
    ← ENNReal.coe_le_coe]
  exact le_iSup₂ (α := ℝ≥0∞) x hx |>.trans ht

Result:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
⊢ SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ spectralRadius ℝ ((algebraMap ℝ A) ↑t - a) ≤ ↑t

Proof state:
case refine_1.intro.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : ↑t - y ∈ {↑t} - spectrum ℝ a
⊢ ↑‖↑t - y‖₊ ≤ ↑t

Tactic:
obtain ⟨hty, hyt⟩ := Set.mem_Icc.mp <| this hy

Result:
case refine_1.intro.intro.intro
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
y : ℝ
hy : y ∈ spectrum ℝ a
hx : ↑t - y ∈ {↑t} - spectrum ℝ a
hty : -↑t ≤ y
hyt : y ≤ ↑t
⊢ ↑‖↑t - y‖₊ ≤ ↑t

Proof state:
case refine_2.h.h
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, ‖↑t - x‖₊ ≤ t
x : ℝ
hx : x ∈ spectrum ℝ a
h_le : -↑t ≤ ↑t - x ∧ ↑t - x ≤ ↑t
⊢ 0 ≤ x

Tactic:
linarith [h_le.2]

Result:
no goals

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
t : ℝ≥0
ht : spectralRadius ℝ a ≤ ↑t
this : spectrum ℝ a ⊆ Set.Icc (-↑t) ↑t
h : ∀ x ∈ spectrum ℝ a, 0 ≤ x
x : ℝ
hx : x ∈ {↑t} - spectrum ℝ a
⊢ ∃ y ∈ spectrum ℝ a, ↑t - y = x

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem one_le_one_div {I : Submodule R A} : 1 ≤ 1 / I ↔ I ≤ 1

Proof state:
case mp
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ 1 ≤ 1 / I → I ≤ 1

case mpr
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ I ≤ 1 → 1 ≤ 1 / I

Tactic:
all_goals intro hI

Result:
case mp
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : 1 ≤ 1 / I
⊢ I ≤ 1

case mpr
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ 1 ≤ 1 / I

Proof state:
case mp
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : 1 ≤ 1 / I
⊢ I ≤ 1

Tactic:
rwa [le_div_iff_mul_le, one_mul] at hI

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ 1 ≤ 1 / I ↔ I ≤ 1

Tactic:
constructor

Result:
case mp
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ 1 ≤ 1 / I → I ≤ 1

case mpr
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ I ≤ 1 → 1 ≤ 1 / I

Proof state:
case mpr
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
⊢ I ≤ 1 → 1 ≤ 1 / I

Tactic:
intro hI

Result:
case mpr
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ 1 ≤ 1 / I

Proof state:
case mpr
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ 1 ≤ 1 / I

Tactic:
rwa [le_div_iff_mul_le, one_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma ψ₂_sq : W.ψ₂ ^ 2 = C W.Ψ₂Sq + 4 * W.toAffine.polynomial

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.ψ₂ ^ 2 = C W.Ψ₂Sq + 4 * W.toAffine.polynomial

Tactic:
rw [C_Ψ₂Sq, sub_add_cancel]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem wittSub_zero : wittSub p 0 = X (0, 0) - X (1, 0)

Proof state:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittSub p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) - X (1, 0))

Tactic:
simp only [wittSub, wittStructureRat, map_sub, rename_X, xInTermsOfW_zero, map_X,
  wittPolynomial_zero, bind₁_X_right, map_wittStructureInt]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ wittSub p 0 = X (0, 0) - X (1, 0)

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (map (Int.castRingHom ℚ)) (wittSub p 0) = (map (Int.castRingHom ℚ)) (X (0, 0) - X (1, 0))
-- Mathlib/RingTheory/Trace/Basic.lean
theorem trace_gen_eq_zero {x : L} (hx : ¬IsIntegral K x) :
    Algebra.trace K K⟮x⟯ (AdjoinSimple.gen K x) = 0

Proof state:
case h.intro.intro.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra

Tactic:
exact subset_adjoin K _ (Set.mem_singleton x)

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯) (gen K x) = 0

Tactic:
rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply]

Result:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)

Proof state:
case h.intro.intro
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ IsIntegral K x

Tactic:
refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_

Result:
case h.intro.intro.refine_1
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ (Subalgebra.toSubmodule K⟮x⟯.toSubalgebra).FG

case h.intro.intro.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra

Proof state:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)
⊢ IsIntegral K x

Tactic:
obtain ⟨s, ⟨b⟩⟩ := hx

Result:
case h.intro.intro
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ IsIntegral K x

Proof state:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)

Tactic:
contrapose! hx

Result:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)
⊢ IsIntegral K x

Proof state:
case h.intro.intro.refine_1
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ (Subalgebra.toSubmodule K⟮x⟯.toSubalgebra).FG

Tactic:
exact (Submodule.fg_iff_finiteDimensional _).mpr (FiniteDimensional.of_fintype_basis b)

Result:
no goals
-- Mathlib/NumberTheory/Dioph.lean
theorem induction {C : Poly α → Prop} (H1 : ∀ i, C (proj i)) (H2 : ∀ n, C (const n))
    (H3 : ∀ f g, C f → C g → C (f - g)) (H4 : ∀ f g, C f → C g → C (f * g)) (f : Poly α) : C f

Proof state:
case mk.const
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
n✝ : ℤ
⊢ C ⟨fun x => n✝, ⋯⟩

Tactic:
apply H2

Result:
no goals

Proof state:
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : Poly α
⊢ C f

Tactic:
obtain ⟨f, pf⟩ := f

Result:
case mk
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
⊢ C ⟨f, pf⟩

Proof state:
case mk.sub
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f f✝ g✝ : (α → ℕ) → ℤ
a✝¹ : IsPoly f✝
a✝ : IsPoly g✝
ihf : C ⟨f✝, a✝¹⟩
ihg : C ⟨g✝, a✝⟩
⊢ C ⟨fun x => f✝ x - g✝ x, ⋯⟩

Tactic:
apply H3 _ _ ihf ihg

Result:
no goals

Proof state:
case mk.mul
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f f✝ g✝ : (α → ℕ) → ℤ
a✝¹ : IsPoly f✝
a✝ : IsPoly g✝
ihf : C ⟨f✝, a✝¹⟩
ihg : C ⟨g✝, a✝⟩
⊢ C ⟨fun x => f✝ x * g✝ x, ⋯⟩

Tactic:
apply H4 _ _ ihf ihg

Result:
no goals

Proof state:
case mk
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
pf : IsPoly f
⊢ C ⟨f, pf⟩

Tactic:
induction pf with
| proj => apply H1
| const => apply H2
| sub _ _ ihf ihg => apply H3 _ _ ihf ihg
| mul _ _ ihf ihg => apply H4 _ _ ihf ihg

Result:
no goals

Proof state:
case mk.proj
α : Type u_1
C : Poly α → Prop
H1 : ∀ (i : α), C (proj i)
H2 : ∀ (n : ℤ), C (const n)
H3 : ∀ (f g : Poly α), C f → C g → C (f - g)
H4 : ∀ (f g : Poly α), C f → C g → C (f * g)
f : (α → ℕ) → ℤ
i✝ : α
⊢ C ⟨fun x => ↑(x i✝), ⋯⟩

Tactic:
apply H1

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem exists_mem_nhds_zero_mul_subset
    {K U : Set M} (hK : IsCompact K) (hU : U ∈ 𝓝 0) : ∃ V ∈ 𝓝 0, K * V ⊆ U

Proof state:
case refine_3.intro.intro.intro.intro
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

Tactic:
use V ∩ W, inter_mem V_in W_in

Result:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
s t V : Set M
V_in : V ∈ 𝓝 0
hV' : s * V ⊆ U
W : Set M
W_in : W ∈ 𝓝 0
hW' : t * W ⊆ U
⊢ (s ∪ t) * (V ∩ W) ⊆ U
-- Mathlib/Data/Set/Lattice.lean
theorem image2_iUnion_left (s : ι → Set α) (t : Set β) :
    image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : ι → Set α
t : Set β
⊢ image2 f (⋃ i, s i) t = ⋃ i, image2 f (s i) t

Tactic:
simp only [← image_prod, iUnion_prod_const, image_iUnion]

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem Equiv.antisymm_iff {l₁ l₂ : Lists' α true} : of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Proof state:
case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
exact ⟨h₁, h₂⟩

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
refine ⟨fun h => ?_, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩

Result:
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Proof state:
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁

Tactic:
simp [Lists'.Subset.refl]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h

Result:
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁

case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem prod_swap : map Prod.swap (μ.prod ν) = ν.prod μ

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : SFinite μ
s : Set (β × α)
hs : MeasurableSet s
⊢ ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) s =
    ∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) s

Tactic:
exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem toBlock_diagonal_disjoint (d : m → α) {p q : m → Prop} (hpq : Disjoint p q) :
    Matrix.toBlock (diagonal d) p q = 0

Proof state:
case a.mk.mk
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩

Result:
case a.mk.mk
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩

Proof state:
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
⊢ (diagonal d).toBlock p q = 0

Tactic:
ext ⟨i, hi⟩ ⟨j, hj⟩

Result:
case a.mk.mk
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩

Proof state:
case a.mk.mk
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p q : m → Prop
hpq : Disjoint p q
i : m
hi : p i
j : m
hj : q j
this : i ≠ j
⊢ (diagonal d).toBlock p q ⟨i, hi⟩ ⟨j, hj⟩ = 0 ⟨i, hi⟩ ⟨j, hj⟩

Tactic:
simp [diagonal_apply_ne d this]

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
/--
Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subset `S ⊆ A`, the centralizer of `S ⊗ 1 ⊆ A ⊗ B` is `C_A(S) ⊗ B` where `C_A(S)` is the
centralizer of `S` in `A`.
-/
lemma centralizer_coe_image_includeLeft_eq_center_tensorProduct
    (S : Set A) [Module.Free R B] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.includeLeft (S := R) '' S) =
    (Algebra.TensorProduct.map (Subalgebra.centralizer R (S : Set A)).val
      (AlgHom.id R B)).range

Proof state:
case h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : (x ⊗ₜ[R] 1 * b.sum fun i m => m ⊗ₜ[R] ℬ i) = (b.sum fun i m => m ⊗ₜ[R] ℬ i) * x ⊗ₜ[R] 1
⊢ x • b = mapRange (fun x_1 => x_1 * x) ⋯ b

Tactic:
simp only [Finsupp.sum, Finset.mul_sum, Algebra.TensorProduct.tmul_mul_tmul, one_mul,
  Finset.sum_mul, mul_one] at hw

Result:
case h.mp.intro
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
hw : ∑ i ∈ b.support, (x * b i) ⊗ₜ[R] ℬ i = ∑ i ∈ b.support, (b i * x) ⊗ₜ[R] ℬ i
⊢ x • b = mapRange (fun x_1 => x_1 * x) ⋯ b
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
theorem powers_eq_top_of_prime_card {p : ℕ}
    [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : Submonoid.powers g = ⊤

Proof state:
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
⊢ Submonoid.powers g = ⊤

Tactic:
ext x

Result:
case h
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
x : G
⊢ x ∈ Submonoid.powers g ↔ x ∈ ⊤

Proof state:
case h
G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g : G
hg : g ≠ 1
x : G
⊢ x ∈ Submonoid.powers g ↔ x ∈ ⊤

Tactic:
simp [mem_powers_of_prime_card h hg]

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem tendsto_toReal {a : EReal} (ha : a ≠ ⊤) (h'a : a ≠ ⊥) :
    Tendsto EReal.toReal (𝓝 a) (𝓝 a.toReal)

Proof state:
case intro
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)

Tactic:
exact tendsto_id

Result:
no goals

Proof state:
a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ Tendsto toReal (𝓝 a) (𝓝 a.toReal)

Tactic:
lift a to ℝ using ⟨ha, h'a⟩

Result:
case intro
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto toReal (𝓝 ↑a) (𝓝 (↑a).toReal)

Proof state:
case intro
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto toReal (𝓝 ↑a) (𝓝 (↑a).toReal)

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Result:
case intro
a : ℝ
ha : ↑a ≠ ⊤
h'a : ↑a ≠ ⊥
⊢ Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)