harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma equation_iff_variableChange (x y : R) :
    W'.Equation x y ↔ (W'.variableChange ⟨1, x, 0, y⟩).toAffine.Equation 0 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)) = 0 ↔
    1 ^ 6 *
        (W'.a₆ + { u := 1, r := x, s := 0, t := y }.r * W'.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W'.a₂ +
                { u := 1, r := x, s := 0, t := y }.r ^ 3 -
              { u := 1, r := x, s := 0, t := y }.t * W'.a₃ -
            { u := 1, r := x, s := 0, t := y }.t ^ 2 -
          { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W'.a₁) =
      0

Tactic:
congr! 1

Result:
case a.h.e'_2
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)) =
    1 ^ 6 *
      (W'.a₆ + { u := 1, r := x, s := 0, t := y }.r * W'.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W'.a₂ +
              { u := 1, r := x, s := 0, t := y }.r ^ 3 -
            { u := 1, r := x, s := 0, t := y }.t * W'.a₃ -
          { u := 1, r := x, s := 0, t := y }.t ^ 2 -
        { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W'.a₁)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ↔ (variableChange W' { u := 1, r := x, s := 0, t := y }).toAffine.Equation 0 0

Tactic:
rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)) = 0 ↔
    1 ^ 6 *
        (W'.a₆ + { u := 1, r := x, s := 0, t := y }.r * W'.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W'.a₂ +
                { u := 1, r := x, s := 0, t := y }.r ^ 3 -
              { u := 1, r := x, s := 0, t := y }.t * W'.a₃ -
            { u := 1, r := x, s := 0, t := y }.t ^ 2 -
          { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W'.a₁) =
      0

Proof state:
case a.h.e'_2
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ -(y ^ 2 + W'.a₁ * x * y + W'.a₃ * y - (x ^ 3 + W'.a₂ * x ^ 2 + W'.a₄ * x + W'.a₆)) =
    1 ^ 6 *
      (W'.a₆ + { u := 1, r := x, s := 0, t := y }.r * W'.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W'.a₂ +
              { u := 1, r := x, s := 0, t := y }.r ^ 3 -
            { u := 1, r := x, s := 0, t := y }.t * W'.a₃ -
          { u := 1, r := x, s := 0, t := y }.t ^ 2 -
        { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W'.a₁)

Tactic:
ring1

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CompactlySupported.lean
@[simp, norm_cast]
lemma coe_finsetInf' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C_c(α, β)) :
    ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i)

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeInf β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i => ⇑(f i)) x✝

Tactic:
simp [finsetInf'_apply]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeInf β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
⊢ ⇑(s.inf' H f) = s.inf' H fun i => ⇑(f i)

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : SemilatticeInf β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : ContinuousInf β
ι : Type u_5
s : Finset ι
H : s.Nonempty
f : ι → α →C_c β
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i => ⇑(f i)) x✝
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma StarOrderedRing.nonneg_iff_spectrum_nonneg [NonnegSpectrumClass R A] (a : A)
    (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.670836) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
⊢ 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x

Tactic:
have := cfc_nonneg_iff (id : R → R) a (by fun_prop) ha

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
this : 0 ≤ cfc id a ↔ ∀ x ∈ spectrum R a, 0 ≤ id x
⊢ 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
this : 0 ≤ cfc id a ↔ ∀ x ∈ spectrum R a, 0 ≤ id x
⊢ 0 ≤ a ↔ ∀ x ∈ spectrum R a, 0 ≤ x

Tactic:
simpa [cfc_id _ a ha] using this

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
⊢ ContinuousOn id (spectrum R a)

Tactic:
fun_prop

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem lt_cof_type [IsWellOrder α r] {S : Set α} : #S < cof (type r) → Bounded r S

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
S : Set α
⊢ #↑S < (type r).cof → Bounded r S

Tactic:
simpa using not_imp_not.2 cof_type_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_append {l₁ : Vector α n₁} {l₂ : Vector α n₂} :
    (l₁ ++ l₂).find? p = (l₁.find? p).or (l₂.find? p)

Proof state:
case mk
α : Type
n₁ n₂ : Nat
p : α → Bool
l₂ : Vector α n₂
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₁
⊢ find? p ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) =
    (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).or (find? p l₂)

Tactic:
cases l₂

Result:
case mk.mk
α : Type
n₁ n₂ : Nat
p : α → Bool
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n₁
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₂
⊢ find? p
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    (find? p { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }).or
      (find? p { toArray := toArray✝, size_toArray := size_toArray✝ })

Proof state:
α : Type
n₁ n₂ : Nat
p : α → Bool
l₁ : Vector α n₁
l₂ : Vector α n₂
⊢ find? p (l₁ ++ l₂) = (find? p l₁).or (find? p l₂)

Tactic:
cases l₁

Result:
case mk
α : Type
n₁ n₂ : Nat
p : α → Bool
l₂ : Vector α n₂
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₁
⊢ find? p ({ toArray := toArray✝, size_toArray := size_toArray✝ } ++ l₂) =
    (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).or (find? p l₂)

Proof state:
case mk.mk
α : Type
n₁ n₂ : Nat
p : α → Bool
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n₁
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n₂
⊢ find? p
      ({ toArray := toArray✝¹, size_toArray := size_toArray✝¹ } ++
        { toArray := toArray✝, size_toArray := size_toArray✝ }) =
    (find? p { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }).or
      (find? p { toArray := toArray✝, size_toArray := size_toArray✝ })

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem ord_preAleph (o : Ordinal) : (preAleph o).ord = preOmega o

Proof state:
o : Ordinal.{u_1}
⊢ (preAleph o).ord = preOmega o

Tactic:
rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]

Result:
no goals
-- Mathlib/LinearAlgebra/StdBasis.lean
lemma piEquiv_apply_apply (ι R M : Type*) [Fintype ι] [CommSemiring R]
    [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → R) :
    piEquiv ι R M v w = ∑ i, w i • v i

Proof state:
ι : Type u_5
R : Type u_6
M : Type u_7
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → R
⊢ ((piEquiv ι R M) v) w = ∑ i : ι, w i • v i

Tactic:
simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]

Result:
ι : Type u_5
R : Type u_6
M : Type u_7
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → R
⊢ ∑ x : ι, ((Pi.basisFun R ι).repr w) x • v x = ∑ i : ι, w i • v i

Proof state:
ι : Type u_5
R : Type u_6
M : Type u_7
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → R
⊢ ∑ x : ι, ((Pi.basisFun R ι).repr w) x • v x = ∑ i : ι, w i • v i

Tactic:
congr

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
theorem of_div (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
    a ≡ b [MOD m]

Proof state:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [MOD m]

Tactic:
convert h.mul_left' c <;> rwa [Nat.mul_div_cancel']

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem nextOr_concat {xs : List α} {x : α} (d : α) (h : x ∉ xs) : nextOr (xs ++ [x]) x d = d

Proof state:
case cons.intro
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : x ∉ []
⊢ ([] ++ [x]).nextOr x d = d

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Tactic:
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)

Result:
case cons.intro
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
hz : ¬x = z
hzs : x ∉ zs
⊢ (z :: zs ++ [x]).nextOr x d = d

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : x ∉ xs
⊢ (xs ++ [x]).nextOr x d = d

Tactic:
induction' xs with z zs IH

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : x ∉ []
⊢ ([] ++ [x]).nextOr x d = d

case cons
α : Type u_1
inst✝ : DecidableEq α
x d z : α
zs : List α
IH : x ∉ zs → (zs ++ [x]).nextOr x d = d
h : x ∉ z :: zs
⊢ (z :: zs ++ [x]).nextOr x d = d
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem length_eq_zero_iff {w : W} : ℓ w = 0 ↔ w = 1

Proof state:
case mp.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.length (cs.wordProd ω) = 0
hω : ω.length = cs.length (cs.wordProd ω)
this : ω = []
⊢ cs.wordProd ω = 1

Tactic:
rw [this, wordProd_nil]

Result:
no goals

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0

Tactic:
exact cs.length_one

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h : cs.length w = 0
⊢ w = 1

Tactic:
rcases cs.exists_reduced_word w with ⟨ω, hω, rfl⟩

Result:
case mp.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.length (cs.wordProd ω) = 0
hω : ω.length = cs.length (cs.wordProd ω)
⊢ cs.wordProd ω = 1

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ w = 1 → cs.length w = 0

Tactic:
rintro rfl

Result:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ cs.length 1 = 0

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 0 ↔ w = 1

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 0 → w = 1

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ w = 1 → cs.length w = 0

Proof state:
case mp.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.length (cs.wordProd ω) = 0
hω : ω.length = cs.length (cs.wordProd ω)
⊢ cs.wordProd ω = 1

Tactic:
have : ω = [] := eq_nil_of_length_eq_zero (hω.trans h)

Result:
case mp.intro.intro
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
h : cs.length (cs.wordProd ω) = 0
hω : ω.length = cs.length (cs.wordProd ω)
this : ω = []
⊢ cs.wordProd ω = 1

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 0 → w = 1

Tactic:
intro h

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
h : cs.length w = 0
⊢ w = 1
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem prod_add : ∀ a b : FactorSet α, (a + b).prod = a.prod * b.prod
  | ⊤, b => show (⊤ + b).prod = (⊤ : FactorSet α).prod * b.prod by simp
  | a, ⊤ => show (a + ⊤).prod = a.prod * (⊤ : FactorSet α).prod by simp
  | WithTop.some a, WithTop.some b => by
    rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : FactorSet α
⊢ (a + ⊤).prod = a.prod * ⊤.prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
⊢ (⊤ + b).prod = ⊤.prod * b.prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a b : Multiset { a // Irreducible a }
⊢ (↑a + ↑b).prod = FactorSet.prod ↑a * FactorSet.prod ↑b

Tactic:
rw [← FactorSet.coe_add, prod_coe, prod_coe, prod_coe, Multiset.map_add, Multiset.prod_add]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_pow_right {n : ℕ} : SameCycle f x ((f ^ n) y) ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
n : ℕ
⊢ f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y

Tactic:
rw [← zpow_natCast, sameCycle_zpow_right]

Result:
no goals
-- Mathlib/NumberTheory/VonMangoldt.lean
theorem vonMangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : Λ (n ^ k) = Λ n

Proof state:
n k : ℕ
hk : k ≠ 0
⊢ Λ (n ^ k) = Λ n

Tactic:
simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk]

Result:
no goals
-- Mathlib/Data/Nat/Count.lean
theorem count_add' (a b : ℕ) : count p (a + b) = count (fun k ↦ p (k + b)) a + count p b

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun k => p (k + b)) a + count p b

Tactic:
rw [add_comm, count_add, add_comm]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k => p (b + k)) a + count p b = count (fun k => p (k + b)) a + count p b

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
⊢ count (fun k => p (b + k)) a + count p b = count (fun k => p (k + b)) a + count p b

Tactic:
simp_rw [add_comm b]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem Measure.withDensityᵥ_absolutelyContinuous (μ : Measure α) (f : α → ℝ) :
    μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
rw [withDensityᵥ, dif_neg hf]

Result:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ 0 ≪ᵥ μ.toENNRealVectorMeasure

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑μ.toENNRealVectorMeasure i = 0
⊢ ↑(μ.withDensityᵥ f) i = 0

Tactic:
rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : μ i = 0
⊢ ↑(μ.withDensityᵥ f) i = 0

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : μ i = 0
⊢ ↑(μ.withDensityᵥ f) i = 0

Tactic:
rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ μ.withDensityᵥ f ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
refine VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => ?_

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑μ.toENNRealVectorMeasure i = 0
⊢ ↑(μ.withDensityᵥ f) i = 0

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ 0 ≪ᵥ μ.toENNRealVectorMeasure

Tactic:
exact VectorMeasure.AbsolutelyContinuous.zero _

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem coeff_mul_left_one_sub_of_lt_weightedOrder
    {d : σ →₀ ℕ} (h : (weight w d) < g.weightedOrder w) :
    coeff R d (f * (1 - g)) = coeff R d f

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ↑((weight w) d) < weightedOrder w (f * g)

Tactic:
exact lt_of_lt_of_le (lt_of_lt_of_le h le_add_self) (le_weightedOrder_mul w)

Result:
no goals

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff R d) (f * g) = 0

Tactic:
apply coeff_eq_zero_of_lt_weightedOrder w

Result:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ ↑((weight w) d) < weightedOrder w (f * g)

Proof state:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff R d) (f * (1 - g)) = (coeff R d) f

Tactic:
simp only [mul_sub, mul_one, _root_.map_sub, sub_eq_self]

Result:
σ : Type u_1
w : σ → ℕ
R : Type u_3
inst✝ : Ring R
f g : MvPowerSeries σ R
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff R d) (f * g) = 0
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem Normal.of_conjugate_fixed {H : Subgroup G} (h : ∀ g : G, (MulAut.conj g) • H = H) :
    H.Normal

Proof state:
case conj_mem
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H

Tactic:
intro n hn g

Result:
case conj_mem
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g * n * g⁻¹ ∈ H

Proof state:
case conj_mem
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H

Tactic:
exact hn

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ H.Normal

Tactic:
constructor

Result:
case conj_mem
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
⊢ ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H

Proof state:
case conj_mem
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g * n * g⁻¹ ∈ H

Tactic:
rw [← h g, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← map_inv, MulAut.smul_def,
  MulAut.conj_apply, inv_inv, mul_assoc, mul_assoc, inv_mul_cancel, mul_one,
  ← mul_assoc, inv_mul_cancel, one_mul]

Result:
case conj_mem
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ n ∈ H
-- Mathlib/Topology/Order.lean
theorem continuous_sSup_dom {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} :
    Continuous[sSup T, t₂] f ↔ ∀ t ∈ T, Continuous[t, t₂] f

Proof state:
α : Type u
β : Type v
f : α → β
T : Set (TopologicalSpace α)
t₂ : TopologicalSpace β
⊢ Continuous f ↔ ∀ t ∈ T, Continuous f

Tactic:
simp only [continuous_iff_le_induced, sSup_le_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/CharacterSpace.lean
theorem union_zero_isClosed [T2Space 𝕜] [ContinuousMul 𝕜] :
    IsClosed (characterSpace 𝕜 A ∪ {0})

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (characterSpace 𝕜 A ∪ {0})

Tactic:
simp only [union_zero, Set.setOf_forall]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : CommSemiring 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : ContinuousAdd 𝕜
inst✝⁵ : ContinuousConstSMul 𝕜 𝕜
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : TopologicalSpace A
inst✝² : Module 𝕜 A
inst✝¹ : T2Space 𝕜
inst✝ : ContinuousMul 𝕜
⊢ IsClosed (⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})

Tactic:
exact
  isClosed_iInter fun x =>
    isClosed_iInter fun y =>
      isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)

Result:
no goals