harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.subtypeCongr.symm : (ep.subtypeCongr en).symm = Perm.subtypeCongr ep.symm en.symm

Proof state:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
⊢ Equiv.symm (ep.subtypeCongr en) = subtypeCongr (Equiv.symm ep) (Equiv.symm en)

Tactic:
ext x

Result:
case H
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Proof state:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑((Equiv.symm ep) ⟨x, h⟩)
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Tactic:
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]

Result:
no goals

Proof state:
case H
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Tactic:
by_cases h : p x

Result:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : p x
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Proof state:
case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑((Equiv.symm en) ⟨x, h⟩)
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Tactic:
simp [Perm.subtypeCongr.apply, h, symm_apply_eq, this]

Result:
no goals

Proof state:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : p x
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Tactic:
have : p (ep.symm ⟨x, h⟩) := Subtype.property _

Result:
case pos
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : p x
this : p ↑((Equiv.symm ep) ⟨x, h⟩)
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Proof state:
case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : ¬p x
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x

Tactic:
have : ¬p (en.symm ⟨x, h⟩) := Subtype.property (en.symm _)

Result:
case neg
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
x : ε
h : ¬p x
this : ¬p ↑((Equiv.symm en) ⟨x, h⟩)
⊢ (Equiv.symm (ep.subtypeCongr en)) x = (subtypeCongr (Equiv.symm ep) (Equiv.symm en)) x
-- Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean
theorem isIdempotentElem_toSubmodule (S : Subalgebra R A) :
    IsIdempotentElem S.toSubmodule

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ toSubmodule S
⊢ x ∈ toSubmodule S * toSubmodule S

Tactic:
rw [← mul_one x]

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ toSubmodule S
⊢ x * 1 ∈ toSubmodule S * toSubmodule S

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ toSubmodule S
⊢ x * 1 ∈ toSubmodule S * toSubmodule S

Tactic:
exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)

Result:
no goals

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S * toSubmodule S ≤ toSubmodule S

Tactic:
refine (mul_toSubmodule_le _ _).trans_eq ?_

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule (S ⊔ S) = toSubmodule S

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ IsIdempotentElem (toSubmodule S)

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S * toSubmodule S ≤ toSubmodule S

case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S ≤ toSubmodule S * toSubmodule S

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule (S ⊔ S) = toSubmodule S

Tactic:
rw [sup_idem]

Result:
no goals

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ toSubmodule S ≤ toSubmodule S * toSubmodule S

Tactic:
intro x hx1

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ toSubmodule S
⊢ x ∈ toSubmodule S * toSubmodule S
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iSup_iff {f : ι → LowerSet α} : (a ∈ ⨆ i, f i) ↔ ∃ i, a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → LowerSet α
⊢ a ∈ ⨆ i, f i ↔ ∃ i, a ∈ f i

Tactic:
rw [← SetLike.mem_coe, coe_iSup]

Result:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → LowerSet α
⊢ a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
a : α
f : ι → LowerSet α
⊢ a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i

Tactic:
exact mem_iUnion

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.einfsep_lt_top (hs : s.Nontrivial) : s.einfsep < ∞

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ⊤

Tactic:
exact hs.einfsep_ne_top

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep < ⊤

Tactic:
rw [lt_top_iff_ne_top]

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ⊤
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem _root_.Real.tendsto_of_bddBelow_antitone {f : ℕ → ℝ} (h_bdd : BddBelow (Set.range f))
    (h_ant : Antitone f) : ∃ r : ℝ, Tendsto f atTop (𝓝 r)

Proof state:
f : ℕ → ℝ
h_bdd : BddBelow (range f)
h_ant : Antitone f
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
obtain ⟨B, hB⟩ := Real.exists_isGLB (Set.range_nonempty f) h_bdd

Result:
case intro
f : ℕ → ℝ
h_bdd : BddBelow (range f)
h_ant : Antitone f
B : ℝ
hB : IsGLB (range f) B
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Proof state:
case intro
f : ℕ → ℝ
h_bdd : BddBelow (range f)
h_ant : Antitone f
B : ℝ
hB : IsGLB (range f) B
⊢ ∃ r, Tendsto f atTop (𝓝 r)

Tactic:
exact ⟨B, tendsto_atTop_isGLB h_ant hB⟩

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
@[simp]
lemma aeval_injective_iff_of_isEmpty [CommSemiring S₁] [Algebra R S₁] {f : σ → S₁} :
    Function.Injective (aeval f : MvPolynomial σ R →ₐ[R] S₁) ↔
      Function.Injective (algebraMap R S₁)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) ↔ Injective (⇑(algebraMap R S₁) ∘ ⇑(isEmptyAlgEquiv R σ))

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑(aeval f) ↔ Injective ⇑(algebraMap R S₁)

Tactic:
rw [this, ← Injective.of_comp_iff' _ (@isEmptyAlgEquiv R σ _ _).bijective]

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) ↔ Injective (⇑(algebraMap R S₁) ∘ ⇑(isEmptyAlgEquiv R σ))

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)

Tactic:
ext i

Result:
case hf
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
i : σ
⊢ (aeval f) (X i) = ((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) (X i)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
⊢ Injective ⇑(aeval f) ↔ Injective ⇑(algebraMap R S₁)

Tactic:
have : aeval f = (Algebra.ofId R S₁).comp (@isEmptyAlgEquiv R σ _ _).toAlgHom := by
  ext i
  exact IsEmpty.elim' ‹IsEmpty σ› i

Result:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
this : aeval f = (Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)
⊢ Injective ⇑(aeval f) ↔ Injective ⇑(algebraMap R S₁)

Proof state:
case hf
R : Type u
S₁ : Type v
σ : Type u_1
inst✝³ : CommSemiring R
inst✝² : IsEmpty σ
inst✝¹ : CommSemiring S₁
inst✝ : Algebra R S₁
f : σ → S₁
i : σ
⊢ (aeval f) (X i) = ((Algebra.ofId R S₁).comp ↑(isEmptyAlgEquiv R σ)) (X i)

Tactic:
exact IsEmpty.elim' ‹IsEmpty σ› i

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem equiv_of_eq {x y : PGame} (h : x = y) : x ≈ y

Proof state:
x y : PGame
h : x = y
⊢ x ≈ y

Tactic:
subst h

Result:
x : PGame
⊢ x ≈ x

Proof state:
x : PGame
⊢ x ≈ x

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_cast_heq {α β} (h : α = β) (s : Finset α) :
    HEq (s.map (Equiv.cast h).toEmbedding) s

Proof state:
α : Type u_4
s : Finset α
⊢ HEq (map (Equiv.cast ⋯).toEmbedding s) s

Tactic:
simp

Result:
no goals

Proof state:
α β : Type u_4
h : α = β
s : Finset α
⊢ HEq (map (Equiv.cast h).toEmbedding s) s

Tactic:
subst h

Result:
α : Type u_4
s : Finset α
⊢ HEq (map (Equiv.cast ⋯).toEmbedding s) s
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem le_iInf₂_lintegral {ι : Sort*} {ι' : ι → Sort*} (f : ∀ i, ι' i → α → ℝ≥0∞) :
    ∫⁻ a, ⨅ (i) (h : ι' i), f i h a ∂μ ≤ ⨅ (i) (h : ι' i), ∫⁻ a, f i h a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
ι' : ι → Sort u_6
f : (i : ι) → ι' i → α → ℝ≥0∞
⊢ ∫⁻ (a : α), ⨅ i, ⨅ h, f i h a ∂μ ≤ ⨅ i, ⨅ h, ∫⁻ (a : α), f i h a ∂μ

Tactic:
convert (monotone_lintegral μ).map_iInf₂_le f with a

Result:
case h.e'_3.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
ι' : ι → Sort u_6
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ ⨅ i, ⨅ h, f i h a = (⨅ i, ⨅ j, f i j) a

Proof state:
case h.e'_3.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_5
ι' : ι → Sort u_6
f : (i : ι) → ι' i → α → ℝ≥0∞
a : α
⊢ ⨅ i, ⨅ h, f i h a = (⨅ i, ⨅ j, f i j) a

Tactic:
simp only [iInf_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_const_left' (a b c : BitVec w) : (a + b) + c = (a + c) + b

Proof state:
w : Nat
a b c : BitVec w
⊢ a + b + c = a + c + b

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma map_inf (L M : Sublattice α) (f : LatticeHom α β) (hf : Injective f) :
    map f (L ⊓ M) = map f L ⊓ map f M

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)

Tactic:
simp [Set.image_inter hf]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L M : Sublattice α
f : LatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_eq_top_iff_finite (s : Set α) :
    span s = ⊤ ↔ ∃ s' : Finset α, ↑s' ⊆ s ∧ span (s' : Set α) = ⊤

Proof state:
α : Type u
inst✝ : Semiring α
s : Set α
⊢ 1 ∈ span s ↔ ∃ s', ↑s' ⊆ s ∧ 1 ∈ span ↑s'

Tactic:
exact ⟨Submodule.mem_span_finite_of_mem_span, fun ⟨s', h₁, h₂⟩ => span_mono h₁ h₂⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
s : Set α
⊢ span s = ⊤ ↔ ∃ s', ↑s' ⊆ s ∧ span ↑s' = ⊤

Tactic:
simp_rw [eq_top_iff_one]

Result:
α : Type u
inst✝ : Semiring α
s : Set α
⊢ 1 ∈ span s ↔ ∃ s', ↑s' ⊆ s ∧ 1 ∈ span ↑s'
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma shatterer_eq : 𝒜.shatterer = 𝒜 ↔ IsLowerSet (𝒜 : Set (Finset α))

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ s ∈ 𝒜

Tactic:
obtain ⟨t, ht, hst⟩ := (mem_shatterer.1 hs).exists_superset

Result:
case refine_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜

Proof state:
case refine_2.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
⊢ s ∈ 𝒜

Tactic:
exact h hst ht

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ 𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet ↑𝒜

case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : IsLowerSet ↑𝒜
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ s ∈ 𝒜

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet ↑𝒜.shatterer

Tactic:
exact isLowerSet_shatterer _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet ↑𝒜

Tactic:
rw [← h]

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
h : 𝒜.shatterer = 𝒜
⊢ IsLowerSet ↑𝒜.shatterer
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_empty {a : α} [Inhabited α] {c} :
    (empty c : Raw₀ α β).getKey! a = default

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
a : α
inst✝ : Inhabited α
c : Nat
⊢ (empty c).getKey! a = default

Tactic:
simp [getKey!, empty]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma leadingCoeff_add_eq_left (h : q.supDegree D < p.supDegree D) :
    (p + q).leadingCoeff D = p.leadingCoeff D

Proof state:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
rw [leadingCoeff, supDegree_add_eq_left h, Finsupp.add_apply, ← leadingCoeff,
  apply_eq_zero_of_not_le_supDegree (D := D), add_zero]

Result:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Tactic:
obtain ⟨a, he⟩ := supDegree_mem_range D (ne_zero_of_not_supDegree_le h.not_le)

Result:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ leadingCoeff D (p + q) = leadingCoeff D p

Proof state:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬D (Function.invFun D (supDegree D p)) ≤ supDegree D q

Tactic:
rw [← he, Function.apply_invFun_apply (f := D), he]

Result:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬supDegree D p ≤ supDegree D q

Proof state:
case intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
he : D a = supDegree D p
⊢ ¬supDegree D p ≤ supDegree D q

Tactic:
exact h.not_le

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma iSup_genWeightSpace_eq_top' [IsTriangularizable K L M] :
    ⨆ χ : Weight K L M, genWeightSpace M χ = ⊤

Proof state:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
this : ⨆ χ, genWeightSpace M χ = ⊤
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤

Tactic:
erw [← iSup_ne_bot_subtype, ← (Weight.equivSetOf K L M).iSup_comp] at this

Result:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
this : ⨆ x, genWeightSpace M ↑((Weight.equivSetOf K L M) x) = ⊤
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤

Proof state:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
this : ⨆ x, genWeightSpace M ↑((Weight.equivSetOf K L M) x) = ⊤
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤

Tactic:
exact this

Result:
no goals

Proof state:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤

Tactic:
have := iSup_genWeightSpace_eq_top K L M

Result:
K : Type u_1
L : Type u_3
M : Type u_4
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieRing.IsNilpotent L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : Module K M
inst✝² : LieModule K L M
inst✝¹ : FiniteDimensional K M
inst✝ : IsTriangularizable K L M
this : ⨆ χ, genWeightSpace M χ = ⊤
⊢ ⨆ χ, genWeightSpace M ⇑χ = ⊤
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_of_isLocallySurjective_fac
    {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} {f₃ : F₁ ⟶ F₃} (fac : f₁ ≫ f₂ = f₃)
    [IsLocallySurjective J f₃] : IsLocallySurjective J f₂

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
⊢ IsLocallySurjective J f₂

Tactic:
exact isLocallySurjective_of_isLocallySurjective J f₁ f₂

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₃
⊢ IsLocallySurjective J f₂

Tactic:
subst fac

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
⊢ IsLocallySurjective J f₂
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
lemma volume_closedBall_of_dim_even {k : ℕ} (hk : finrank ℝ E = 2 * k) (x : E) (r : ℝ) :
    volume (closedBall x r) = .ofReal r ^ finrank ℝ E * .ofReal (π ^ k / (k : ℕ)!)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nontrivial E
k : ℕ
hk : finrank ℝ E = 2 * k
x : E
r : ℝ
⊢ volume (closedBall x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (π ^ k / ↑k !)

Tactic:
rw [addHaar_closedBall_eq_addHaar_ball, volume_ball_of_dim_even hk x]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_inv_le_iff_of_pos (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 < z) : x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : 0 < z
⊢ x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

Tactic:
rw [← rpow_le_rpow_iff _ hy hz, rpow_inv_rpow] <;> positivity

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
theorem face_centroid_eq_centroid {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ}
    (h : #fs = m + 1) : Finset.univ.centroid k (s.face h).points = fs.centroid k s.points

Proof state:
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = Set.range ⇑(fs.orderEmbOfFin h).toEmbedding

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ fs = map (fs.orderEmbOfFin h).toEmbedding univ

Tactic:
rw [← Finset.coe_inj, Finset.coe_map, Finset.coe_univ, Set.image_univ]

Result:
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ↑fs = Set.range ⇑(fs.orderEmbOfFin h).toEmbedding

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ centroid k univ (s.face h).points = centroid k fs s.points

Tactic:
convert (Finset.univ.centroid_map k (fs.orderEmbOfFin h).toEmbedding s.points).symm

Result:
case h.e'_3.h.e'_9
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
n : ℕ
s : Simplex k P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ fs = map (fs.orderEmbOfFin h).toEmbedding univ