harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem ext_linear_iff {f g : P1 →ᵃ[k] P2} : f = g ↔ (f.linear = g.linear) ∧ (∃ p, f p = g p) :=
  ⟨fun h ↦ ⟨congrArg _ h, by inhabit P1; exact default, by rw [h]⟩,
  fun h ↦ Exists.casesOn h.2 fun _ hp ↦ ext_linear h.1 hp⟩

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
⊢ f default = g default

Tactic:
rw [h]

Result:
no goals

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
inhabited_h : Inhabited P1
⊢ P1

Tactic:
exact default

Result:
no goals

Proof state:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
⊢ P1

Tactic:
inhabit P1

Result:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V1
inst✝⁴ : Module k V1
inst✝³ : AffineSpace V1 P1
inst✝² : AddCommGroup V2
inst✝¹ : Module k V2
inst✝ : AffineSpace V2 P2
f g : P1 →ᵃ[k] P2
h : f = g
inhabited_h : Inhabited P1
⊢ P1
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem Transcendental.aeval_of_transcendental {r : A} (H : Transcendental R r)
    {f : R[X]} (hf : Transcendental R f) : Transcendental R (Polynomial.aeval r f)

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0
⊢ p = 0

Tactic:
exact hf _ (H _ (by rwa [← aeval_comp, comp_eq_aeval] at hp))

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0
⊢ (Polynomial.aeval r) ((Polynomial.aeval f) p) = 0

Tactic:
rwa [← aeval_comp, comp_eq_aeval] at hp

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : Transcendental R r
f : R[X]
hf : Transcendental R f
⊢ Transcendental R ((Polynomial.aeval r) f)

Tactic:
rw [transcendental_iff] at H hf ⊢

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
⊢ ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
⊢ ∀ (p : R[X]), (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0 → p = 0

Tactic:
intro p hp

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
H : ∀ (p : R[X]), (Polynomial.aeval r) p = 0 → p = 0
f : R[X]
hf : ∀ (p : R[X]), (Polynomial.aeval f) p = 0 → p = 0
p : R[X]
hp : (Polynomial.aeval ((Polynomial.aeval r) f)) p = 0
⊢ p = 0
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.exists_eq_pow_mul_and_not_dvd (hfin : FiniteMultiplicity a b) :
    ∃ c : α, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
obtain ⟨c, hc⟩ := pow_multiplicity_dvd a b

Result:
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Proof state:
case intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ False

Tactic:
exact (hfin.multiplicity_eq_iff.1 (by simp)).2 h₁

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
⊢ False

Tactic:
have h₁ : a ^ (multiplicity a b + 1) ∣ b := ⟨k, hc⟩

Result:
case intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ False

Proof state:
case intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
⊢ False

Tactic:
rw [hk, ← mul_assoc, ← _root_.pow_succ] at hc

Result:
case intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
⊢ False

Proof state:
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ∃ c, b = a ^ multiplicity a b * c ∧ ¬a ∣ c

Tactic:
refine ⟨c, hc, ?_⟩

Result:
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ¬a ∣ c

Proof state:
case intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
⊢ ¬a ∣ c

Tactic:
rintro ⟨k, hk⟩

Result:
case intro.intro
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c : α
hc : b = a ^ multiplicity a b * c
k : α
hk : c = a * k
⊢ False

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
hfin : FiniteMultiplicity a b
c k : α
hc : b = a ^ (multiplicity a b + 1) * k
hk : c = a * k
h₁ : a ^ (multiplicity a b + 1) ∣ b
⊢ multiplicity a b = multiplicity a b

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem mul_congr_left {a b : Int} (h₁ : a = b)  (c : Int) : a * c = b * c

Proof state:
a b : Int
h₁ : a = b
c : Int
⊢ a * c = b * c

Tactic:
subst h₁

Result:
a c : Int
⊢ a * c = a * c

Proof state:
a c : Int
⊢ a * c = a * c

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
theorem Int.mem_zmultiples_iff {a b : ℤ} : b ∈ AddSubgroup.zmultiples a ↔ a ∣ b :=
  exists_congr fun k => by rw [mul_comm, eq_comm, ← smul_eq_mul]

Proof state:
a b k : ℤ
⊢ (fun x => x • a) k = b ↔ b = a * k

Tactic:
rw [mul_comm, eq_comm, ← smul_eq_mul]

Result:
no goals
-- Mathlib/Control/Traversable/Equiv.lean
theorem comp_traverse (f : β → F γ) (g : α → G β) (x : t' α) :
    Equiv.traverse eqv (Comp.mk ∘ Functor.map f ∘ g) x =
      Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Equiv.traverse eqv (Comp.mk ∘ map f ∘ g) x = Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
rw [traverse_def, comp_traverse, Comp.map_mk]

Result:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk ((fun x => ⇑(eqv γ) <$> x) <$> traverse f <$> traverse g ((eqv α).symm x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Proof state:
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝⁵ : Traversable t
inst✝⁴ : LawfulTraversable t
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
x : t' α
⊢ Comp.mk ((fun x => ⇑(eqv γ) <$> x) <$> traverse f <$> traverse g ((eqv α).symm x)) =
    Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)

Tactic:
simp only [map_map, Function.comp_def, traverse_def, symm_apply_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_setIfInBounds_self (v : Vector α n) (i : Nat) (x : α) :
    (v.setIfInBounds i x)[i]? = if i < n then some x else none

Proof state:
α : Type u_1
n : Nat
v : Vector α n
i : Nat
x : α
⊢ (v.setIfInBounds i x)[i]? = if i < n then some x else none

Tactic:
simp [getElem?_setIfInBounds]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Multiplication.lean
lemma P24_neg_left : P24 x₁ x₂ y ↔ P24 (-x₂) (-x₁) y

Proof state:
x₁ x₂ y : PGame
⊢ P24 x₁ x₂ y ↔ P24 (-x₂) (-x₁) y

Tactic:
rw [P24, P24, P2_neg_left, P4_neg_left]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelIso_hom_desc {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    (w : f ≫ g = 0) :
    (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w

Tactic:
ext1

Result:
case h
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w

Proof state:
case h
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelπ f ≫ explicitCokernelDesc w

Tactic:
simp [explicitCokernelDesc, explicitCokernelπ, explicitCokernelIso,
  IsColimit.coconePointUniqueUpToIso]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem of_results_think {s : Computation α} {a n} (h : Results (think s) a n) :
    ∃ m, Results s a m ∧ n = m + 1

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
haveI := of_think_terminates h.terminates

Result:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this : s.Terminates
⊢ ∃ m, s.Results a m ∧ n = m + 1

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this : s.Terminates
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
have := results_of_terminates' _ (of_think_mem h.mem)

Result:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this✝ : s.Terminates
this : s.Results a s.length
⊢ ∃ m, s.Results a m ∧ n = m + 1

Proof state:
α : Type u
s : Computation α
a : α
n : ℕ
h : s.think.Results a n
this✝ : s.Terminates
this : s.Results a s.length
⊢ ∃ m, s.Results a m ∧ n = m + 1

Tactic:
exact ⟨_, this, Results.len_unique h (results_think this)⟩

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- `x⁻¹` is analytic away from zero -/
lemma analyticOnNhd_inv : AnalyticOnNhd 𝕜 (fun z ↦ z⁻¹) {z : 𝕝 | z ≠ 0}

Proof state:
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
z : 𝕝
m : z ∈ {z | z ≠ 0}
⊢ AnalyticAt 𝕜 (fun z => z⁻¹) z

Tactic:
exact analyticAt_inv m

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
⊢ AnalyticOnNhd 𝕜 (fun z => z⁻¹) {z | z ≠ 0}

Tactic:
intro z m

Result:
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_7
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
z : 𝕝
m : z ∈ {z | z ≠ 0}
⊢ AnalyticAt 𝕜 (fun z => z⁻¹) z
-- Mathlib/Data/Nat/Log.lean
theorem add_pred_div_lt {b n : ℕ} (hb : 1 < b) (hn : 2 ≤ n) : (n + b - 1) / b < n

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < n + b

Tactic:
omega

Result:
no goals

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ (n + b - 1) / b < n

Tactic:
rw [div_lt_iff_lt_mul (by omega), ← succ_le_iff, ← pred_eq_sub_one,
  succ_pred_eq_of_pos (by omega)]

Result:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ n + b ≤ n * b

Tactic:
exact Nat.add_le_mul hn hb

Result:
no goals

Proof state:
b n : ℕ
hb : 1 < b
hn : 2 ≤ n
⊢ 0 < b

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Ultra.lean
@[to_additive]
lemma nnnorm_pow_le (x : S) (n : ℕ) :
    ‖x ^ n‖₊ ≤ ‖x‖₊

Proof state:
case succ
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
n : ℕ
hn : ‖x ^ n‖₊ ≤ ‖x‖₊
⊢ ‖x ^ (n + 1)‖₊ ≤ ‖x‖₊

Tactic:
simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
⊢ ‖x ^ 0‖₊ ≤ ‖x‖₊

Tactic:
simp

Result:
no goals

Proof state:
S : Type u_1
inst✝¹ : SeminormedGroup S
inst✝ : IsUltrametricDist S
x : S
n : ℕ
⊢ ‖x ^ n‖₊ ≤ ‖x‖₊

Tactic:
induction n with
| zero => simp
| succ n hn => simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x

Result:
no goals
-- Mathlib/RingTheory/Unramified/LocalRing.lean
@[stacks 00UW "(1)"]
lemma FormallyUnramified.map_maximalIdeal [FormallyUnramified R S] :
    (maximalIdeal R).map (algebraMap R S) = maximalIdeal S

Proof state:
case hI
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ (Ideal.map (algebraMap R S) (maximalIdeal R)).IsMaximal

Tactic:
rw [Ideal.Quotient.maximal_ideal_iff_isField_quotient]

Result:
case hI
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S

Tactic:
apply eq_maximalIdeal

Result:
case hI
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ (Ideal.map (algebraMap R S) (maximalIdeal R)).IsMaximal

Proof state:
case hI
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : FormallyUnramified R S
⊢ IsField (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))

Tactic:
exact isField_quotient_map_maximalIdeal

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_add (hq : 0 ≤ q) (hp : 0 ≤ p) : toNNRat (q + p) = toNNRat q + toNNRat p :=
  NNRat.ext <| by simp [toNNRat, hq, hp, add_nonneg]

Proof state:
p q : ℚ
hq : 0 ≤ q
hp : 0 ≤ p
⊢ ↑(q + p).toNNRat = ↑(q.toNNRat + p.toNNRat)

Tactic:
simp [toNNRat, hq, hp, add_nonneg]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem attach_cons (a : α) (m : Multiset α) :
    (a ::ₘ m).attach =
      ⟨a, mem_cons_self a m⟩ ::ₘ m.attach.map fun p => ⟨p.1, mem_cons_of_mem p.2⟩ :=
  Quotient.inductionOn m fun l =>
    congr_arg _ <|
      congr_arg (List.cons _) <| by
        rw [List.map_pmap]; exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.eq rfl

Proof state:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.pmap (fun a_1 h => ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯

Tactic:
exact List.pmap_congr_left _ fun _ _ _ _ => Subtype.eq rfl

Result:
no goals

Proof state:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.map (fun p => ⟨↑p, ⋯⟩) (List.pmap mk l ⋯)

Tactic:
rw [List.map_pmap]

Result:
α : Type u_1
a : α
m : Multiset α
l : List α
⊢ List.pmap mk l ⋯ = List.pmap (fun a_1 h => ⟨↑⟨a_1, h⟩, ⋯⟩) l ⋯
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem algebraMap_apply (h : IsAdjoinRoot S f) (x : R) :
    algebraMap R S x = h.map (Polynomial.C x)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRoot S f
x : R
⊢ (algebraMap R S) x = h.map (C x)

Tactic:
rw [h.algebraMap_eq, RingHom.comp_apply]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
lemma sum_sq_le_sq_sum_of_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) :
    ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ x ∈ s, f x * f x ≤ ∑ i ∈ s, ∑ j ∈ s, f i * f j

Tactic:
refine sum_le_sum fun i hi ↦ ?_

Result:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ ∑ j ∈ s, f i * f j

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i

Tactic:
gcongr

Result:
case a0
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ 0 ≤ f i

case h
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ≤ ∑ i ∈ s, f i

Proof state:
case h
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ≤ ∑ i ∈ s, f i

Tactic:
exact single_le_sum hf hi

Result:
no goals

Proof state:
case a0
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ 0 ≤ f i

Tactic:
exact hf i hi

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, f i ^ 2 ≤ (∑ i ∈ s, f i) ^ 2

Tactic:
simp only [sq, sum_mul_sum]

Result:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ x ∈ s, f x * f x ≤ ∑ i ∈ s, ∑ j ∈ s, f i * f j

Proof state:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ ∑ j ∈ s, f i * f j

Tactic:
rw [← mul_sum]

Result:
ι : Type u_1
R : Type u_2
inst✝ : OrderedSemiring R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_rw₂ {f₁ f₁' : α → β} {f₂ f₂' : α → γ} (h₁ : f₁ =ᵐ[μ] f₁') (h₂ : f₂ =ᵐ[μ] f₂')
    (g : β → γ → ℝ≥0∞) : ∫⁻ a, g (f₁ a) (f₂ a) ∂μ = ∫⁻ a, g (f₁' a) (f₂' a) ∂μ :=
  lintegral_congr_ae <| h₁.mp <| h₂.mono fun _ h₂ h₁ => by dsimp only; rw [h₁, h₂]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᶠ[ae μ] f₁'
h₂✝ : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ (fun a => g (f₁ a) (f₂ a)) x✝ = (fun a => g (f₁' a) (f₂' a)) x✝

Tactic:
dsimp only

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᶠ[ae μ] f₁'
h₂✝ : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ g (f₁ x✝) (f₂ x✝) = g (f₁' x✝) (f₂' x✝)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᶠ[ae μ] f₁'
h₂✝ : f₂ =ᶠ[ae μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ g (f₁ x✝) (f₂ x✝) = g (f₁' x✝) (f₂' x✝)

Tactic:
rw [h₁, h₂]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_top_smul_measure (hT : DominatedFinMeasAdditive (∞ • μ) T C) (f : α → E) :
    setToFun (∞ • μ) T hT f = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
⊢ setToFun (⊤ • μ) T hT f = 0

Tactic:
refine setToFun_measure_zero' hT fun s _ hμs => ?_

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : (⊤ • μ) s < ⊤
⊢ (⊤ • μ) s = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : (⊤ • μ) s < ⊤
⊢ (⊤ • μ) s = 0

Tactic:
rw [lt_top_iff_ne_top] at hμs

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : (⊤ • μ) s ≠ ⊤
⊢ (⊤ • μ) s = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : (⊤ • μ) s ≠ ⊤
⊢ (⊤ • μ) s = 0

Tactic:
simp only [true_and, Measure.smul_apply, ENNReal.mul_eq_top, eq_self_iff_true,
  top_ne_zero, Ne, not_false_iff, not_or, Classical.not_not, smul_eq_mul] at hμs

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ¬μ s = ⊤ ∧ μ s = 0
⊢ (⊤ • μ) s = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive (⊤ • μ) T C
f : α → E
s : Set α
x✝ : MeasurableSet s
hμs : ¬μ s = ⊤ ∧ μ s = 0
⊢ (⊤ • μ) s = 0

Tactic:
simp only [hμs.right, Measure.smul_apply, mul_zero, smul_eq_mul]

Result:
no goals