mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: case refine_2.refine_3
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x y : A ⊗[R] B
m : M
⊢ ∀ (x y : A ⊗[R] B),
    (∀ (x_1 : A) (y : B), (x_1 ⊗ₜ[R] y * x) • m = x_1 ⊗ₜ[R] y • x • m) →
      (∀ (x : A) (y_1 : B), (x ⊗ₜ[R] y_1 * y) • m = x ⊗ₜ[R] y_1 • y • m) →
        ∀ (x_1 : A) (y_1 : B), (x_1 ⊗ₜ[R] y_1 * (x + y)) • m = x_1 ⊗ₜ[R] y_1 • (x + y) • m

Tactic:
intro z w hz hw a b
      -- Porting note: was one `simp only`, but random stuff doesn't work
      simp only [(· • ·)] at hz hw ⊢
      simp only [moduleAux_apply, mul_add, map_add,
        LinearMap.add_apply, moduleAux_apply, hz, hw]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Maps

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ (f a * 1) ⊗ₜ[R] g b ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)

Tactic:
← one_mul (g b),

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
f : A →ₐ[R] C
g : B →ₐ[R] D
a : A
b : B
⊢ (f a * 1) ⊗ₜ[R] (1 * g b) ∈ ↑((includeLeft.comp f).range ⊔ (includeRight.comp g).range)
Module: Mathlib.Algebra.Algebra.Unitization

Goal state before:
pp: case inl_add_inr
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : SMulCommClass R A A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : NonUnitalSemiring B
inst✝⁴ : StarRing B
inst✝³ : Module R B
inst✝² : SMulCommClass R B B
inst✝¹ : IsScalarTower R B B
inst✝ : StarModule R B
φ : A →⋆ₙₐ[R] B
hφ : Function.Surjective ⇑φ
r : R
b : B
⊢ ∃ a, (starMap φ) a = inl r + ↑b

Tactic:
| inl_add_inr r b =>

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case e'_3.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
y : ↥(centralizer R S) ⊗[R] A
hy : (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y = (Algebra.TensorProduct.comm R A B) x
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A))
      ((Algebra.TensorProduct.comm R A ↥(centralizer R S)) ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A) y)) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y

Tactic:
← Algebra.TensorProduct.comm_symm,

Goal state after:
case e'_3.mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set B
inst✝ : Module.Free R A
eq1 :
  comap (↑(Algebra.TensorProduct.comm R A B)) (centralizer R (⇑includeLeft '' S)) =
    comap (↑(Algebra.TensorProduct.comm R A B)) (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)).range
x : A ⊗[R] B
y : ↥(centralizer R S) ⊗[R] A
hy : (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y = (Algebra.TensorProduct.comm R A B) x
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A))
      ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A).symm
        ((Algebra.TensorProduct.comm R (↥(centralizer R S)) A) y)) =
    (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R A)) y
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max v w u, v} #m * lift.{max v w u, w} #n

Tactic:
← lift_lift.{v, max u w},

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
m : Type v
n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ lift.{max u w, v} #m * lift.{max u v, w} #n = lift.{max u w, v} (lift.{v, v} #m) * lift.{max v w u, w} #n
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι →₀ R) = card ι

Tactic:
rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
← lift_inj,

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : lift.{?u.64, v} (Module.rank R ↥(span R (range b))) = lift.{?u.64, v} #↑(range b)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
Module: Mathlib.LinearAlgebra.Dimension.Constructions

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = ↑(Fintype.card ι)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)

Tactic:
lift_eq_nat_iff

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
⊢ Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
Module: Mathlib.Algebra.Star.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
S✝ S T : NonUnitalStarSubalgebra R A
h : (fun S ↦ S.toNonUnitalSubalgebra) S = (fun S ↦ S.toNonUnitalSubalgebra) T
⊢ ∀ (x : A), x ∈ S ↔ x ∈ T

Tactic:
apply SetLike.ext_iff.1 h

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_1
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ g ∘ₗ p.subtype = f

pp: case refine_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ g v = y

Tactic:
· ext x
    have := LinearPMap.supSpanSingleton_apply_mk_of_mem ⟨p, f⟩ y hv x.2
    simpa using! congr($hg _).trans this

Goal state after:
case refine_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
p : Submodule K V
v : V
f : ↥p →ₗ[K] V'
hv : v ∉ p
y : V'
g : V →ₗ[K] V'
hg :
  g ∘ₗ ({ domain := p, toFun := f }.supSpanSingleton v y hv).domain.subtype =
    ({ domain := p, toFun := f }.supSpanSingleton v y hv).toFun
⊢ g v = y
Module: Mathlib.RingTheory.Finiteness.Lattice

Goal state before:
pp: case intro
R : Type u_2
V : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup V
inst✝² : Module R V
ι : Sort u_1
inst✝¹ : Finite ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
val✝ : Fintype (PLift ι)
⊢ Module.Finite R ↥(⨆ i, S i.down)

Tactic:
← Finset.sup_univ_eq_iSup

Goal state after:
case intro
R : Type u_2
V : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup V
inst✝² : Module R V
ι : Sort u_1
inst✝¹ : Finite ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
val✝ : Fintype (PLift ι)
⊢ Module.Finite R ↥(Finset.univ.sup fun i ↦ S i.down)
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ ↑f (c • ⟨x, hfx⟩) = ↑g ⟨c • x, ⋯⟩

Tactic:
this hgx,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ ↑f (c • ⟨x, hfx⟩) = ↑g (c • ⟨x, hgx⟩)
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
⊢ ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x

Tactic:
let eQ' := W'.prodEquivOfIsCompl Q' hQ'

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W W' : Submodule K V
inst✝ : FiniteDimensional K ↥W
f : ↥W ≃ₗ[K] ↥W'
Q : Submodule K V
hQ : IsCompl W Q
eQ : (↥W × ↥Q) ≃ₗ[K] V := W.prodEquivOfIsCompl Q hQ
Q' : Submodule K V
hQ' : IsCompl W' Q'
eQ' : (↥W' × ↥Q') ≃ₗ[K] V := W'.prodEquivOfIsCompl Q' hQ'
⊢ ∃ g, ∀ (x : ↥W), ↑(f x) = g ↑x
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ Module.rank K ↥s ≤ 1 ↔ ∃ v₀ ∈ s, s ≤ K ∙ v₀

Tactic:
simp_rw [rank_le_one_iff, le_span_singleton_iff]

Goal state after:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Submodule K V
inst✝ : Free K ↥s
⊢ (∃ v₀, ∀ (v : ↥s), ∃ r, r • v₀ = v) ↔ ∃ v₀ ∈ s, ∀ v ∈ s, ∃ r, r • v₀ = v
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ + 0 = Quot.mk (Rel R X) a✝

Tactic:
change Quot.mk _ _ = _

Goal state after:
case mk
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (a✝ + 0) = Quot.mk (Rel R X) a✝
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: case pos
n : ℕ
n2 : 2 ≤ n
x✝ : ℕ
k : ℕ := x✝
i : ℕ
e : x✝ = 2 * i + 3
a : ∀ (m : ℕ), 2 ≤ m → m ∣ n → x✝ ≤ m
h : n < k * k
⊢ n.minFacProp (if n < x✝ * x✝ then n else if x✝ ∣ n then x✝ else n.minFacAux (x✝ + 2))

Tactic:
have pp : Prime n :=
        prime_def_le_sqrt.2
          ⟨n2, fun m m2 l d => not_lt_of_ge l <| lt_of_lt_of_le (sqrt_lt.2 h) (a m m2 d)⟩
      simpa only [k, h] using
        ⟨n2, dvd_rfl, fun m m2 d => le_of_eq ((dvd_prime_two_le pp m2).1 d).symm⟩

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (z • f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

Tactic:
mem_graph_iff

Goal state after:
case mp
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
h : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr.mk
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : (fst✝, snd✝) ∈ f.graph
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
⊢ (x_fst, x_snd) ∈ (z • f).graph

Tactic:
mem_graph_iff

Goal state after:
case mpr.mk
R : Type u_1
inst✝⁷ : Ring R
E : Type u_4
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module R E
F : Type u_5
inst✝⁴ : AddCommGroup F
M : Type u_7
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : Module R F
inst✝ : SMulCommClass R M F
f : E →ₗ.[R] F
z : M
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2
h : fst✝ = x_fst ∧ z • snd✝ = x_snd
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(z • f) y = (x_fst, x_snd).2
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : (x_fst, x_snd) ∈ (-f).graph
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph

Tactic:
mem_graph_iff

Goal state after:
case mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
h : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ Submodule.map (LinearMap.id.prodMap (-LinearMap.id)) f.graph
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case mpr.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : (fst✝, snd✝) ∈ f.graph
h : fst✝ = x_fst ∧ -snd✝ = x_snd
⊢ (x_fst, x_snd) ∈ (-f).graph

Tactic:
mem_graph_iff

Goal state after:
case mpr.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x_fst : E
x_snd : F
fst✝ : E
snd✝ : F
hx' : ∃ y, ↑y = (fst✝, snd✝).1 ∧ ↑f y = (fst✝, snd✝).2
h : fst✝ = x_fst ∧ -snd✝ = x_snd
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑(-f) y = (x_fst, x_snd).2
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : x ∈ f.graph
⊢ x ∈ g.graph

Tactic:
mem_graph_iff

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f ≤ g
x : E × F
hx : ∃ y, ↑y = x.1 ∧ ↑f y = x.2
⊢ ∃ y, ↑y = x.1 ∧ ↑g y = x.2
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x : ↥(map (LinearMap.fst R E F) g)
⊢ (↑x, ↑g.toLinearPMap x) ∈ g

Tactic:
rw [toLinearPMap_apply_aux hg]
  exact valFromGraph_mem hg x.2

Goal state after:
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∑ x ∈ range (n + 1), (X ^ x).coeff k * r ^ (n - x) * ↑(n.choose x) = r ^ (n - k) * ↑(n.choose k)

Tactic:
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]

Goal state after:
case h₀
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ ∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0

case h₁
R : Type u
inst✝ : Semiring R
r : R
n k : ℕ
⊢ k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
inst✝ : Nonempty A
hD : Function.Injective D
a : A
r : R
hr : ¬r = 0
⊢ (single a r).coeff (Function.invFun D (D a)) = r

Tactic:
· rw [Function.leftInverse_invFun hD]
    simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
⊢ p.natDegree = 0

Tactic:
obtain ⟨q, hq⟩ := h.exists_right_inv

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
a✝ : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ p.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ (X ^ n + C (-a)).degree = ↑n

Tactic:
degree_X_pow_add_C hn

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ ↑n = ↑n
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
x✝ : ∃ a b, a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ u + v = embDomain f y

Tactic:
← hw,

Goal state after:
case refine_1
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
f : α ↪ β
y : α →₀ ℕ
u v : β →₀ ℕ
x✝ : ∃ a b, a + b = y ∧ embDomain f a = u ∧ embDomain f b = v
w z : α →₀ ℕ
h : w + z = y
hw : embDomain f w = u
hz : embDomain f z = v
⊢ embDomain f w + v = embDomain f y
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι → κ
h : Function.Injective f
f1 f2 : ι →₀ α
y : κ
hy : y ∈ Set.range f
⊢ (mapDomain f (f1 - f2)) y = (mapDomain f f1 - mapDomain f f2) y

Tactic:
· obtain ⟨x, rfl⟩ := hy
    simp [mapDomain_apply h]

Goal state after:
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
by
  ext
  simp [imp_iff_not_or]

Goal state after:
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case e'_1.e'_3
R : Type u
inst✝¹ : CommRing R
p q : R[X]
a b : R
inst✝ : Invertible a
⊢ p = (algEquivCMulXAddC a b) (p.comp (C ⅟a * (X - C b)))

Tactic:
simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]

Goal state after:
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊔ g).support = f.support ∪ g.support

Tactic:
by
  ext
  simp [imp_iff_not_or]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * (X n ^ 1 * (monomial s) a))

Tactic:
pow_one,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p✝ : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : σ
ih : ∀ {s : σ →₀ ℕ} {a : R}, eval₂ f g (p * (monomial s) a) = eval₂ f g p * f a * s.prod fun n e ↦ g n ^ e
s : σ →₀ ℕ
a : R
⊢ eval₂ f g (p * X n * (monomial s) a) = eval₂ f g (p * (X n * (monomial s) a))
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
⊢ e ≠ 0 → motive ((monomial p) a) → motive ((monomial (Finsupp.single n e + p)) a)

Tactic:
_he

Goal state after:
case single_add
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
motive : MvPolynomial σ R → Prop
C : ∀ (a : R), motive (MvPolynomial.C a)
mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
⊢ motive ((monomial p) a) → motive ((monomial (Finsupp.single n e + p)) a)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p ^ 1) = eval₂ f g p ^ (n + 1)

Tactic:
pow_one,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p) = eval₂ f g p ^ (n + 1)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * eval₂ f g p ^ 1

Tactic:
pow_one,

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
n : ℕ
⊢ eval₂ f g (p ^ n * p) = eval₂ f g p ^ n * eval₂ f g p
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m ((monomial (Finsupp.single i k)) 1) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0

Tactic:
@monomial_eq _ _ (1 : R) (Finsupp.single i k) _,

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
m : σ →₀ ℕ
k : ℕ
this : coeff m (C 1 * (Finsupp.single i k).prod fun n e ↦ X n ^ e) = if Finsupp.single i k = m then 1 else 0
⊢ coeff m (X i ^ k) = if Finsupp.single i k = m then 1 else 0