harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_preimage_mem_nhds' {x x' : M} (h : x' ∈ (extChartAt I x).source)
    (ht : t ∈ 𝓝 x') : (extChartAt I x).symm ⁻¹' t ∈ 𝓝 (extChartAt I x x') :=
  extend_preimage_mem_nhds _ (by rwa [← extChartAt_source I]) ht

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
t : Set M
inst✝ : ChartedSpace H M
x x' : M
h : x' ∈ (extChartAt I x).source
ht : t ∈ 𝓝 x'
⊢ x' ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source I]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_eq_bot_iff : map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
g : Filter β
⊢ map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥

Tactic:
simp [← map_prod_eq_map₂]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_self (hs : s.Finite) (hs' : s.Nonempty) : uniformOn s s = 1

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ (uniformOn s) s = 1

Tactic:
rw [uniformOn, cond_apply hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]

Result:
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ 0

case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ ⊤

Proof state:
case h0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ 0

Tactic:
rwa [Measure.count_ne_zero_iff]

Result:
no goals

Proof state:
case ht
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Measure.count s ≠ ⊤

Tactic:
exact (Measure.count_apply_lt_top.2 hs).ne

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem exp_eq_one_iff : exponent G = 1 ↔ Subsingleton G

Proof state:
case ge.h
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 0 < exponent G

Tactic:
apply exponent_pos_of_exists 1 Nat.one_pos

Result:
case ge.h
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1

Proof state:
case ge
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 1 ≤ exponent G

Tactic:
apply Nat.succ_le_of_lt

Result:
case ge.h
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 0 < exponent G

Proof state:
case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a = b

Tactic:
rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]

Result:
no goals

Proof state:
case ge.h
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
G : Type u
inst✝ : Monoid G
⊢ exponent G = 1 ↔ Subsingleton G

Tactic:
refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩

Result:
case a_eq_b
G : Type u
inst✝ : Monoid G
eq_one : exponent G = 1
a b : G
⊢ a = b

case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ exponent G ≤ 1

case ge
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ 1 ≤ exponent G

Proof state:
case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ exponent G ≤ 1

Tactic:
apply exponent_min' _ Nat.one_pos

Result:
case le
G : Type u
inst✝ : Monoid G
h : Subsingleton G
⊢ ∀ (g : G), g ^ 1 = 1
-- Mathlib/Combinatorics/Additive/SmallTripling.lean
@[to_additive]
private lemma small_neg_neg_pos_mul (hA : #(A ^ 3) ≤ K * #A) : #(A⁻¹ * A⁻¹ * A) ≤ K ^ 2 * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A ^ 3)) ≤ K * ↑(#A)

Tactic:
simpa

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)⁻¹) ≤ K ^ 2 * ↑(#A)

Tactic:
simpa [mul_assoc] using small_neg_pos_pos_mul (A := A) (K := K) (by simpa)

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)) ≤ K ^ 2 * ↑(#A)

Tactic:
rw [← card_inv]

Result:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)⁻¹) ≤ K ^ 2 * ↑(#A)
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem topologicalSpace_eq [UniformSpace F] [UniformAddGroup F] (𝔖 : Set (Set E)) :
    instTopologicalSpace σ F 𝔖 = TopologicalSpace.induced (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe)
      (UniformOnFun.topologicalSpace E F 𝔖)

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

Tactic:
congr

Result:
case e_t.h.e_3.h
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ IsTopologicalAddGroup.toUniformSpace F = inst✝¹

Proof state:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ instTopologicalSpace σ F 𝔖 =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

Tactic:
rw [instTopologicalSpace]

Result:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ TopologicalSpace.induced DFunLike.coe (UniformOnFun.topologicalSpace E F 𝔖) =
    TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe) (UniformOnFun.topologicalSpace E F 𝔖)

Proof state:
case e_t.h.e_3.h
𝕜₁ : Type u_1
𝕜₂ : Type u_2
inst✝⁸ : NormedField 𝕜₁
inst✝⁷ : NormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
E : Type u_3
F : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜₁ E
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜₂ F
inst✝¹ : UniformSpace F
inst✝ : UniformAddGroup F
𝔖 : Set (Set E)
⊢ IsTopologicalAddGroup.toUniformSpace F = inst✝¹

Tactic:
exact UniformAddGroup.toUniformSpace_eq

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean
theorem covariant_flip_iff [h : Std.Commutative mu] :
    Covariant N N (flip mu) r ↔ Covariant N N mu r

Proof state:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (flip mu) r ↔ Covariant N N mu r

Tactic:
unfold flip

Result:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (fun b a => mu a b) r ↔ Covariant N N mu r

Proof state:
N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (fun b a => mu a b) r ↔ Covariant N N mu r

Tactic:
simp_rw [h.comm]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem isometry_intCast : Isometry ((↑) : ℤ → ℂ) :=
  Isometry.of_dist_eq <| by simp_rw [← Complex.ofReal_intCast,
    Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]

Proof state:
⊢ ∀ (x y : ℤ), dist ↑x ↑y = dist x y

Tactic:
simp_rw [← Complex.ofReal_intCast,
Complex.isometry_ofReal.dist_eq, Int.dist_cast_real, implies_true]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem finrank_eq_zero_of_basis_imp_not_finite
    (h : ∀ s : Set M, Basis.{v} (s : Set M) R M → ¬s.Finite) : finrank R M = 0

Proof state:
case inr
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Nontrivial R
⊢ finrank R M = 0

Tactic:
obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set R M).mp ‹_›

Result:
case inr.intro.intro
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
⊢ finrank R M = 0

Proof state:
case inr.intro.intro
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
this : Infinite ↑w✝
⊢ finrank R M = 0

Tactic:
exact b.linearIndependent.finrank_eq_zero_of_infinite

Result:
no goals

Proof state:
case inr.intro.intro
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
⊢ finrank R M = 0

Tactic:
have := Set.Infinite.to_subtype (h _ b)

Result:
case inr.intro.intro
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Nontrivial R
w✝ : Set M
b : Basis (↑w✝) R M
this : Infinite ↑w✝
⊢ finrank R M = 0

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Subsingleton R
⊢ finrank R M = 0

Tactic:
have := Module.subsingleton R M

Result:
case inl
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Subsingleton R
this : Subsingleton M
⊢ finrank R M = 0

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Subsingleton R
this : Subsingleton M
⊢ finrank R M = 0

Tactic:
exact (h ∅ ⟨LinearEquiv.ofSubsingleton _ _⟩ Set.finite_empty).elim

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
⊢ finrank R M = 0

Tactic:
cases subsingleton_or_nontrivial R

Result:
case inl
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Subsingleton R
⊢ finrank R M = 0

case inr
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite
h✝ : Nontrivial R
⊢ finrank R M = 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_take (s : String) (n : Nat) : (s.take n).1 = s.1.take n

Proof state:
s : String
n : Nat
⊢ (s.take n).data = List.take n s.data

Tactic:
rw [take_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem abs_rpow_le_exp_log_mul (x y : ℝ) : |x ^ y| ≤ exp (log x * y)

Proof state:
x y : ℝ
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
by_cases hx : x = 0

Result:
case pos
x y : ℝ
hx : x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

case neg
x y : ℝ
hx : ¬x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Proof state:
x y : ℝ
⊢ |x ^ y| ≤ rexp (log x * y)

Tactic:
refine (abs_rpow_le_abs_rpow x y).trans ?_

Result:
x y : ℝ
⊢ |x| ^ y ≤ rexp (log x * y)

Proof state:
case pos
x y : ℝ
hx : x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
by_cases hy : y = 0 <;> simp [hx, hy, zero_le_one]

Result:
no goals

Proof state:
case neg
x y : ℝ
hx : ¬x = 0
⊢ |x| ^ y ≤ rexp (log x * y)

Tactic:
rw [rpow_def_of_pos (abs_pos.2 hx), log_abs]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_preΨ' (n : ℕ) : (W.baseChange B).preΨ' n = ((W.baseChange A).preΨ' n).map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℕ
⊢ (W.baseChange B).preΨ' n = Polynomial.map (↑f) ((W.baseChange A).preΨ' n)

Tactic:
rw [← map_preΨ', map_baseChange]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.post_desc (c : Cocone F) :
    colimit.post F G ≫ G.map (colimit.desc F c) = colimit.desc (F ⋙ G) (G.mapCocone c)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
⊢ post F G ≫ G.map (desc F c) = desc (F ⋙ G) (G.mapCocone c)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝

Tactic:
rfl

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝
-- Mathlib/RingTheory/Generators.lean
lemma ofComp_kerCompPreimage (Q : Generators S T) (P : Generators R S) (x : Q.ker) :
    (Q.ofComp P).toAlgHom (kerCompPreimage Q P x) = x

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i => (Q.ofComp P).toAlgHom ((X ∘ Sum.inr) i)) (P.σ (↑x j)) *
      j.prod fun a b => (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

Tactic:
simp only [ofComp_val, Sum.elim_inr, Function.comp_apply, self_val, id_eq,
  Sum.elim_inl, monomial_eq, Hom.toAlgHom_X]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
x : ↥Q.ker
j : Q.vars →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i => C (P.val i)) (P.σ (↑x j)) * j.prod fun a b => X a ^ b) = C (coeff j ↑x) * j.prod fun n e => X n ^ e
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem map_comp {f : α → β} {g : β → γ} : map (g ∘ f) = (map g).comp (map f) :=
  Eq.symm <| lift.ext _ _ fun _ ↦ by simp [map]

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x✝ : α
⊢ ((map g).comp (map f)) (of x✝) = (map (g ∘ f)) (of x✝)

Tactic:
simp [map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem ae_withDensity_iff' {p : α → Prop} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) :
    (∀ᵐ x ∂μ.withDensity f, p x) ↔ ∀ᵐ x ∂μ, f x ≠ 0 → p x

Proof state:
case e_a.h.e_6.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ {x | f x ≠ 0} ∩ {a | ¬p a} = {a | ¬(f a ≠ 0 → p a)}

Tactic:
ext x

Result:
case e_a.h.e_6.h.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ {a | ¬p a} ↔ x ∈ {a | ¬(f a ≠ 0 → p a)}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ ({x | f x ≠ 0} ∩ {a | ¬p a}) = 0) = (μ {a | ¬(f a ≠ 0 → p a)} = 0)

Tactic:
congr

Result:
case e_a.h.e_6.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ {x | f x ≠ 0} ∩ {a | ¬p a} = {a | ¬(f a ≠ 0 → p a)}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x

Tactic:
rw [ae_iff, ae_iff, withDensity_apply_eq_zero' hf, iff_iff_eq]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ (μ ({x | f x ≠ 0} ∩ {a | ¬p a}) = 0) = (μ {a | ¬(f a ≠ 0 → p a)} = 0)

Proof state:
case e_a.h.e_6.h.h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ {a | ¬p a} ↔ x ∈ {a | ¬(f a ≠ 0 → p a)}

Tactic:
simp only [exists_prop, mem_inter_iff, mem_setOf_eq, not_forall]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_vsub (w₁ w₂ : ι → k) (p : ι → P) :
    s.affineCombination k p w₁ -ᵥ s.affineCombination k p w₂ = s.weightedVSub p (w₁ - w₂)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w₁ w₂ : ι → k
p : ι → P
⊢ (affineCombination k s p) w₁ -ᵥ (affineCombination k s p) w₂ = (s.weightedVSub p) (w₁ - w₂)

Tactic:
rw [← AffineMap.linearMap_vsub, affineCombination_linear, vsub_eq_sub]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem one_lt_exp_iff {x : ℝ} : 1 < exp x ↔ 0 < x

Proof state:
x : ℝ
⊢ 1 < rexp x ↔ 0 < x

Tactic:
rw [← exp_zero, exp_lt_exp]

Result:
no goals
-- Mathlib/Tactic/Ring/RingNF.lean
theorem rat_rawCast_pos {R} [DivisionRing R] :
    (Rat.rawCast (.ofNat n) d : R) = Nat.rawCast n / Nat.rawCast d

Proof state:
n d : ℕ
R : Type u_2
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.ofNat n) d = n.rawCast / d.rawCast

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
@[to_additive]
lemma prod_Ioi_mul_eq_prod_Ici (a : α) : (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Proof state:
α : Type u_1
M : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid M
f : α → M
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Tactic:
rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma nnrpow_sqrt {a : A} {x : ℝ≥0} : (sqrt a) ^ x = a ^ (x / 2)

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
x : ℝ≥0
⊢ sqrt a ^ x = a ^ (x / 2)

Tactic:
rw [sqrt_eq_nnrpow, nnrpow_nnrpow, one_div_mul_eq_div 2 x]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem forall_mem_range {p : α → Prop} : (∀ a ∈ range f, p a) ↔ ∀ i, p (f i)

Proof state:
α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∀ a ∈ range f, p a) ↔ ∀ (i : ι), p (f i)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma IsTotallyUnimodular.apply {A : Matrix m n R} (hA : A.IsTotallyUnimodular) (i : m) (j : n) :
    A i j ∈ Set.range SignType.cast

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : A.IsTotallyUnimodular
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast

Tactic:
rw [isTotallyUnimodular_iff] at hA

Result:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast

Proof state:
m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
i : m
j : n
⊢ A i j ∈ Set.range SignType.cast

Tactic:
simpa using hA 1 (fun _ => i) (fun _ => j)

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem comp_inj' {p₁ p₂ : Path a b} {q₁ q₂ : Path b c} (h : p₁.length = p₂.length) :
    p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂ :=
  ⟨fun h_eq => (comp_inj <| Nat.add_left_cancel (n := p₂.length) <|
    by simpa [h] using congr_arg length h_eq).1 h_eq,
   by rintro ⟨rfl, rfl⟩; rfl⟩

Proof state:
case intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
h : p₁.length = p₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
⊢ p₁ = p₂ ∧ q₁ = q₂ → p₁.comp q₁ = p₂.comp q₂

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
h : p₁.length = p₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Proof state:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
q₁ q₂ : Path b c
h : p₁.length = p₂.length
h_eq : p₁.comp q₁ = p₂.comp q₂
⊢ p₂.length + q₁.length = p₂.length + q₂.length

Tactic:
simpa [h] using congr_arg length h_eq

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_X_sub_C (a : R) : degree (X - C a) = 1

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
a : R
⊢ (X - C a).degree = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem inf_iSup_eq (a : α) (f : ι → α) : (a ⊓ ⨆ i, f i) = ⨆ i, a ⊓ f i

Proof state:
α : Type u
ι : Sort w
inst✝ : Frame α
a : α
f : ι → α
⊢ a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i

Tactic:
simpa only [inf_comm] using iSup_inf_eq f a

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem IsOpenEmbedding.tendsto_nhds_iff' (hf : IsOpenEmbedding f) {l : Filter Z} {x : X} :
    Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rw [Tendsto, ← map_map, hf.map_nhds_eq]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ map g (𝓝 (f x)) ≤ l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem Specializes.pow {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M]
    {a b : M} (h : a ⤳ b) (n : ℕ) : (a ^ n) ⤳ (b ^ n) :=
  Nat.recOn n (by simp only [pow_zero, specializes_rfl]) fun _ ihn ↦ by
    simpa only [pow_succ] using ihn.mul h

Proof state:
M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n x✝ : ℕ
ihn : (a ^ x✝) ⤳ (b ^ x✝)
⊢ (a ^ x✝.succ) ⤳ (b ^ x✝.succ)

Tactic:
simpa only [pow_succ] using ihn.mul h

Result:
no goals

Proof state:
M : Type u_6
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a b : M
h : a ⤳ b
n : ℕ
⊢ (a ^ Nat.zero) ⤳ (b ^ Nat.zero)

Tactic:
simp only [pow_zero, specializes_rfl]

Result:
no goals