harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean
theorem contMDiffOn_extChartAt_symm (x : M) :
    ContMDiffOn 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target

Proof state:
case h.e'_23
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ (extChartAt I x).target = ↑I '' (chartAt H x).target

Tactic:
rw [extChartAt_target, I.image_eq]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ ContMDiffOn 𝓘(𝕜, E) I n (↑(extChartAt I x).symm) (extChartAt I x).target

Tactic:
convert contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)

Result:
case h.e'_23
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ (extChartAt I x).target = ↑I '' (chartAt H x).target

case convert_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ IsManifold I n M

case convert_3
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ IsManifold I n M

Proof state:
case convert_3
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ IsManifold I n M

Tactic:
infer_instance

Result:
no goals

Proof state:
case convert_1
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : WithTop ℕ∞
inst✝ : IsManifold I n M
x : M
⊢ IsManifold I n M

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem ContinuousWithinAt.of_dslope (h : ContinuousWithinAt (dslope f a) s b) :
    ContinuousWithinAt f s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
⊢ ContinuousWithinAt f s b

Tactic:
have : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b :=
  ((continuousWithinAt_id.sub continuousWithinAt_const).smul h).add continuousWithinAt_const

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
this : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b
⊢ ContinuousWithinAt f s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : ContinuousWithinAt (dslope f a) s b
this : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b
⊢ ContinuousWithinAt f s b

Tactic:
simpa only [sub_smul_dslope, sub_add_cancel] using this

Result:
no goals
-- Mathlib/Topology/Connected/TotallyDisconnected.lean
lemma Topology.IsEmbedding.isTotallyDisconnected_range [TopologicalSpace β] {f : α → β}
    (hf : IsEmbedding f) : IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsEmbedding f
⊢ IsTotallyDisconnected (range f) ↔ TotallyDisconnectedSpace α

Tactic:
rw [totallyDisconnectedSpace_iff, ← image_univ, hf.isTotallyDisconnected_image]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem summable_one_div_pow_of_le {m : ℝ} {f : ℕ → ℕ} (hm : 1 < m) (fi : ∀ i, i ≤ f i) :
    Summable fun i ↦ 1 / m ^ f i

Proof state:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a

Tactic:
rw [div_pow, one_pow]

Result:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a

Proof state:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a

Tactic:
refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a)) <;>
  exact pow_pos (zero_lt_one.trans hm) _

Result:
no goals

Proof state:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable fun i => 1 / m ^ f i

Tactic:
refine .of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
    (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
      ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))

Result:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a

Proof state:
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 ≤ 1 / m ^ f a

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem nnnorm_inv (a : α) : ‖a⁻¹‖₊ = ‖a‖₊⁻¹ :=
  NNReal.eq <| by simp

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
a : α
⊢ ↑‖a⁻¹‖₊ = ↑‖a‖₊⁻¹

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/Circle.lean
@[norm_cast] lemma coe_eq_one : (x : ℂ) = 1 ↔ x = 1

Proof state:
x : Circle
⊢ ↑x = 1 ↔ x = 1

Tactic:
rw [← coe_inj, coe_one]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_pow_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a : M₀
n : ℕ
ha : 0 ≤ a
hn : n ≠ 0
⊢ 1 < a ^ n ↔ 1 < a

Tactic:
simpa only [one_pow] using pow_lt_pow_iff_left₀ zero_le_one ha hn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem tan_int_mul_pi_div_two (n : ℤ) : tan (n * π / 2) = 0 :=
  tan_eq_zero_iff.mpr (by use n)

Proof state:
n : ℤ
⊢ ∃ k, ↑k * ↑π / 2 = ↑n * ↑π / 2

Tactic:
use n

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
@[simp]
lemma eHolderNorm_const (r : ℝ≥0) (c : Y) : eHolderNorm r (Function.const X c) = 0

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ∀ b > ⊥, ∃ i, ∃ (_ : HolderWith i r (Function.const X c)), ↑i < b

Tactic:
exact fun C' hC' => ⟨0, .const, hC'⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ eHolderNorm r (Function.const X c) = 0

Tactic:
rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ∀ b > ⊥, ∃ i, ∃ (_ : HolderWith i r (Function.const X c)), ↑i < b
-- Mathlib/Algebra/Group/Action/Equidecomp.lean
theorem IsDecompOn.comp {g f : X → X} {B A : Set X} {T S : Finset G}
    (hg : IsDecompOn g B T) (hf : IsDecompOn f A S) (h : MapsTo f A B) :
    IsDecompOn (g ∘ f) A (T * S)

Proof state:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) A (T * S)

Tactic:
rw [left_eq_inter.mpr h]

Result:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) (A ∩ fun a => B (f a)) (T * S)

Proof state:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) (A ∩ fun a => B (f a)) (T * S)

Tactic:
exact hg.comp' hf

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem absConvexHull_eq_empty : absConvexHull 𝕜 s = ∅ ↔ s = ∅

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ (absConvexHull 𝕜) s = ∅ ↔ s = ∅

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ (absConvexHull 𝕜) s = ∅ → s = ∅

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ s = ∅ → (absConvexHull 𝕜) s = ∅

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
h : (absConvexHull 𝕜) s = ∅
⊢ s ⊆ (absConvexHull 𝕜) s

Tactic:
exact subset_absConvexHull

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ (absConvexHull 𝕜) s = ∅ → s = ∅

Tactic:
intro h

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
h : (absConvexHull 𝕜) s = ∅
⊢ s = ∅

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
⊢ s = ∅ → (absConvexHull 𝕜) s = ∅

Tactic:
rintro rfl

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
⊢ (absConvexHull 𝕜) ∅ = ∅

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
h : (absConvexHull 𝕜) s = ∅
⊢ s = ∅

Tactic:
rw [← Set.subset_empty_iff, ← h]

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
h : (absConvexHull 𝕜) s = ∅
⊢ s ⊆ (absConvexHull 𝕜) s

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
⊢ (absConvexHull 𝕜) ∅ = ∅

Tactic:
exact absConvexHull_empty

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem rightRel_r_eq_rightCosetEquivalence :
    ⇑(QuotientGroup.rightRel s) = RightCosetEquivalence s

Proof state:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝

Tactic:
exact (rightCoset_eq_iff s).symm

Result:
no goals

Proof state:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (rightRel s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝

Tactic:
rw [rightRel_eq]

Result:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ⇑(rightRel s) = RightCosetEquivalence ↑s

Tactic:
ext

Result:
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (rightRel s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulSupport_mulIndicator :
    Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f :=
  ext fun x => by simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]

Proof state:
α : Type u_1
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
x : α
⊢ x ∈ mulSupport (s.mulIndicator f) ↔ x ∈ s ∩ mulSupport f

Tactic:
simp [Function.mem_mulSupport, mulIndicator_apply_eq_one]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem mem_prod_iff_left {s : Set (α × β)} :
    s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ y in g, ∀ x ∈ t, (x, y) ∈ s

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
refine exists_congr fun _ => Iff.rfl.and <| Iff.trans ?_ exists_mem_subset_iff

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
x✝ : Set α
⊢ (∃ t₂ ∈ g, ∀ x ∈ x✝, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x | (fun y => ∀ x ∈ x✝, (x, y) ∈ s) x}

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
x✝ : Set α
⊢ (∃ t₂ ∈ g, ∀ x ∈ x✝, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ g, t ⊆ {x | (fun y => ∀ x ∈ x✝, (x, y) ∈ s) x}

Tactic:
exact exists_congr fun _ => Iff.rfl.and forall₂_swap

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ s ∈ f ×ˢ g ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s

Tactic:
simp only [mem_prod_iff, prod_subset_iff]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α × β)
⊢ (∃ t₁ ∈ f, ∃ t₂ ∈ g, ∀ x ∈ t₁, ∀ y ∈ t₂, (x, y) ∈ s) ↔ ∃ t ∈ f, ∀ᶠ (y : β) in g, ∀ x ∈ t, (x, y) ∈ s
-- Mathlib/Tactic/CongrExclamation.lean
theorem heq_imp_of_eq_imp {α : Sort*} {x y : α} {p : HEq x y → Prop}
    (h : (he : x = y) → p (heq_of_eq he)) (he : HEq x y) : p he

Proof state:
case refl
α : Sort u_1
x : α
p : HEq x x → Prop
h : ∀ (he : x = x), p ⋯
⊢ p ⋯

Tactic:
exact h rfl

Result:
no goals

Proof state:
α : Sort u_1
x y : α
p : HEq x y → Prop
h : ∀ (he : x = y), p ⋯
he : HEq x y
⊢ p he

Tactic:
cases he

Result:
case refl
α : Sort u_1
x : α
p : HEq x x → Prop
h : ∀ (he : x = x), p ⋯
⊢ p ⋯
-- Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean
lemma centralizer_tensorProduct_eq_center_tensorProduct_left [Module.Free R B] :
    Subalgebra.centralizer R
      (Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range =
    (Algebra.TensorProduct.map (Subalgebra.center R A).val (AlgHom.id R B)).range

Proof state:
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
inst✝ : Module.Free R B
⊢ centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = centralizer R ↑includeLeft.range

Tactic:
simp [Algebra.TensorProduct.map_range]

Result:
no goals

Proof state:
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
inst✝ : Module.Free R B
⊢ centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range =
    (Algebra.TensorProduct.map (center R A).val (AlgHom.id R B)).range

Tactic:
rw [← centralizer_coe_range_includeLeft_eq_center_tensorProduct]

Result:
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
inst✝ : Module.Free R B
⊢ centralizer R ↑(Algebra.TensorProduct.map (AlgHom.id R A) (Algebra.ofId R B)).range = centralizer R ↑includeLeft.range
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem map_injective (f : L →ₐ[K] L') : Function.Injective (map f)

Proof state:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : map f a₁✝ = map f a₂✝
⊢ a₁✝ = a₂✝

Tactic:
rwa [← toSubalgebra_injective.eq_iff, toSubalgebra_map, toSubalgebra_map,
  (Subalgebra.map_injective f.injective).eq_iff, toSubalgebra_inj] at h

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
⊢ Function.Injective (map f)

Tactic:
intro _ _ h

Result:
K : Type u_1
L : Type u_2
L' : Type u_3
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Field L'
inst✝¹ : Algebra K L
inst✝ : Algebra K L'
f : L →ₐ[K] L'
a₁✝ a₂✝ : IntermediateField K L
h : map f a₁✝ = map f a₂✝
⊢ a₁✝ = a₂✝
-- Mathlib/.lake/packages/batteries/Batteries/Control/Lawful/MonadLift.lean
theorem monadLift_seqLeft [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β) :
    monadLift (x <* y) = (monadLift x : n α) <* (monadLift y : n β)

Proof state:
m : Type u_1 → Type u_2
n : Type u_1 → Type u_3
inst✝⁵ : Monad m
inst✝⁴ : Monad n
inst✝³ : MonadLiftT m n
inst✝² : LawfulMonadLiftT m n
α β : Type u_1
inst✝¹ : LawfulMonad m
inst✝ : LawfulMonad n
x : m α
y : m β
⊢ monadLift (x <* y) = monadLift x <* monadLift y

Tactic:
simp only [seqLeft_eq, monadLift_map, monadLift_seq]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDerivWithin_sub
    (hf : ContDiffWithinAt 𝕜 n f s x) (hg : ContDiffWithinAt 𝕜 n g s x) :
    iteratedDerivWithin n (f - g) s x =
      iteratedDerivWithin n f s x - iteratedDerivWithin n g s x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
f g : 𝕜 → F
hf : ContDiffWithinAt 𝕜 (↑n) f s x
hg : ContDiffWithinAt 𝕜 (↑n) g s x
⊢ iteratedDerivWithin n (f - g) s x = iteratedDerivWithin n f s x - iteratedDerivWithin n g s x

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, Pi.neg_def, iteratedDerivWithin_add hx h hf hg.neg,
  iteratedDerivWithin_neg']

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_iSup {p : α → Prop} {fs : β → Filter α} :
    (∃ᶠ x in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ x in fs b, p x

Proof state:
α : Type u
β : Type v
p : α → Prop
fs : β → Filter α
⊢ (∃ᶠ (x : α) in ⨆ b, fs b, p x) ↔ ∃ b, ∃ᶠ (x : α) in fs b, p x

Tactic:
simp only [Filter.Frequently, eventually_iSup, not_forall]

Result:
no goals
-- Mathlib/Topology/Connected/LocPathConnected.lean
theorem isOpen_isPathConnected_basis (x : X) :
    (𝓝 x).HasBasis (fun s : Set X ↦ IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hus : u ⊆ s
hu : IsOpen u
hxu : x ∈ u
⊢ ∃ i, (IsOpen i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
exact ⟨pathComponentIn x u, ⟨hu.pathComponentIn _, ⟨mem_pathComponentIn_self hxu,
  isPathConnected_pathComponentIn hxu⟩⟩, pathComponentIn_subset.trans hus⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
⊢ (𝓝 x).HasBasis (fun s => IsOpen s ∧ x ∈ s ∧ IsPathConnected s) id

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨u, hu⟩ ↦ mem_nhds_iff.mpr ⟨u, hu.2, hu.1.1, hu.1.2.1⟩⟩⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ i, (IsOpen i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ ∃ i, (IsOpen i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s

Tactic:
have ⟨u, hus, hu, hxu⟩ := mem_nhds_iff.mp hs

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocPathConnectedSpace X
x : X
s : Set X
hs : s ∈ 𝓝 x
u : Set X
hus : u ⊆ s
hu : IsOpen u
hxu : x ∈ u
⊢ ∃ i, (IsOpen i ∧ x ∈ i ∧ IsPathConnected i) ∧ id i ⊆ s
-- Mathlib/Logic/Function/Basic.lean
lemma forall_update_iff (f : ∀a, β a) {a : α} {b : β a} (p : ∀a, β a → Prop) :
    (∀ x, p x (update f a b x)) ↔ p a b ∧ ∀ x, x ≠ a → p x (f x)

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∀ (x : α), p x (update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
rw [← and_forall_ne a, update_self]

Result:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Order/RelClasses.lean
theorem not_bounded_iff {r : α → α → Prop} (s : Set α) : ¬Bounded r s ↔ Unbounded r s

Proof state:
α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s

Tactic:
simp only [Bounded, Unbounded, not_forall, not_exists, exists_prop, not_and, not_not]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Cast.lean
theorem Hom.cast_eq_cast {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v) :
    e.cast hu hv = _root_.cast (by {rw [hu, hv]}) e

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')

Tactic:
rw [hu, hv]

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ cast ⋯ ⋯ e = _root_.cast ⋯ e

Tactic:
rfl

Result:
no goals

Proof state:
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e = _root_.cast ⋯ e

Tactic:
subst_vars

Result:
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ cast ⋯ ⋯ e = _root_.cast ⋯ e
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_sum {k' G' : Type*} [AddCommMonoid k'] {f : SkewMonoidAlgebra k G}
    {g : G → k → SkewMonoidAlgebra k' G'} {a₂ : G'} :
    (f.sum g).coeff a₂ = f.sum fun a₁ b ↦ (g a₁ b).coeff a₂

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
⊢ (f.sum g).coeff a₂ = f.sum fun a₁ b => (g a₁ b).coeff a₂

Tactic:
simp_rw [coeff, toFinsupp_sum', sum_def, Finsupp.sum_apply]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
theorem fg_of_fg_toSubalgebra (S : IntermediateField F E) (h : S.toSubalgebra.FG) : S.FG

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
h : S.FG
⊢ S.FG

Tactic:
obtain ⟨t, ht⟩ := h

Result:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
t : Finset E
ht : Algebra.adjoin F ↑t = S.toSubalgebra
⊢ S.FG

Proof state:
case intro
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : IntermediateField F E
t : Finset E
ht : Algebra.adjoin F ↑t = S.toSubalgebra
⊢ S.FG

Tactic:
exact ⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem subset_generated (c d : C) : X c d ⊆ (generated X).arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ X c d ⊆ (generated X).arrows c d

Tactic:
dsimp only [generated, sInf]

Result:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ X c d ⊆ ⋂ S ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, S.arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ ∀ i ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, X c d ⊆ i.arrows c d

Tactic:
exact fun S hS f fS => hS _ _ fS

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ X c d ⊆ ⋂ S ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, S.arrows c d

Tactic:
simp only [subset_iInter₂_iff]

Result:
C : Type u
inst✝ : Groupoid C
X : (c d : C) → Set (c ⟶ d)
c d : C
⊢ ∀ i ∈ {S | ∀ (c d : C), X c d ⊆ S.arrows c d}, X c d ⊆ i.arrows c d