mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
⊢ map f 0 = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
s : Finset ι
x : ι → R[M]
⊢ map f (∑ i ∈ s, x i) = ∑ i ∈ s, map f (x i)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
r : R
m : M
⊢ map f (single m r) = single m (f r)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝ : Semiring R
x : R[M]
⊢ map (AddMonoidHom.id R) x = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
⊢ comapDomain f hf 0 = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
m : M
r : R
⊢ comapDomain f hf (single (f m) r) = single m r

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
⊢ mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id R[M]

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[M]
⊢ (fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x) = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[N]
⊢ (fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x) = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x y : R[M]
⊢ mapDomain (⇑e) (x + y) = mapDomain (⇑e) x + mapDomain (⇑e) y

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
⊢ mapDomainAddEquiv R (e₁.trans e₂) = (mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : R[M]
⊢ map (↑e.symm) (map (↑e) x) = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : S[M]
⊢ map (↑e) (map (↑e.symm) x) = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e₁ : M ≃* N
e₂ : N ≃* O
⊢ mapDomainRingEquiv R (e₁.trans e₂) = (mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
e₁ : R ≃+* S
e₂ : S ≃+* T
⊢ mapRingEquiv M (e₁.trans e₂) = (mapRingEquiv M e₁).trans (mapRingEquiv M e₂)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x : R[M]
⊢ map f (-x) = -map f x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : R[M]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff))
      ((fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff)) x) =
    x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : MonoidAlgebra R (Multiplicative M)
⊢ (fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff)) x) =
    x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
⊢ erase m 0 = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
r : R
⊢ erase m (single m r) = 0

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : R[M]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff))
      ((fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff)) x) =
    x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
A : Type u_8
inst✝ : SMulZeroClass A R
a : A
m : M
r : R
⊢ a • single m r = single m (a • r)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : AddMonoidAlgebra R (Additive M)
⊢ (fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff)) x) =
    x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
f : R[M]
⊢ f.coeff.sum single = f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case pos
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : x.coeff p.1 = 0
⊢ x.coeff p.1 * y.coeff p.2 = 0

Tactic:
h1,

Goal state after:
case pos
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
p : M × M
hps : p ∈ s
hp : p ∈ s → x.coeff p.1 ≠ 0 → y.coeff p.2 = 0
h1 : x.coeff p.1 = 0
⊢ 0 * y.coeff p.2 = 0
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
x : M
⊢ MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r : R
⊢ single m (-r) = -single m r

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r s : R
⊢ single m (r - s) = single m r - single m s

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
⊢ univ⁻¹ = univ

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
by
  constructor
  · contrapose! +distrib
    rintro (hs | rfl)
    · exact hs.pow
    · simp
  · rintro ⟨rfl, hn⟩
    exact empty_pow hn

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ ⇑(RelEmbedding.trans (Fin.castOrderIso ⋯).toOrderEmbedding i.succAboveOrderEmb) = ⇑({i}ᶜ.orderEmbOfFin h)

Tactic:
convert!
    orderEmbOfFin_unique _ (fun x ↦ ?_) ((Fin.strictMono_succAbove _).comp (Fin.cast_strictMono _))

Goal state after:
case convert_3
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
x : Fin k
⊢ (i.succAbove ∘ Fin.cast ?convert_7) x ∈ {i}ᶜ

case convert_7
n : ℕ
i : Fin (n + 1)
k : ℕ
h : #{i}ᶜ = k
⊢ k = n
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
⊢ B.repr ((algebraMap R S) r) = Finsupp.single i r

Tactic:
ext j

Goal state after:
R : Type u
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : B i = 1
r : R
j : ι
⊢ (B.repr ((algebraMap R S) r)) j = (Finsupp.single i r) j
Module: Mathlib.LinearAlgebra.FreeModule.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
⊢ ∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x

Tactic:
by_cases! Subsingleton M

Goal state after:
case pos
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Subsingleton M
⊢ ∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x

case neg
R : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
f : End R M
h : ∀ (g : End R M) (x : M), g (f x) = f (g x)
h✝ : Nontrivial M
⊢ ∃ α, ∃ (h : ∀ (g : R), g * α = α * g), ∀ (x : M), f x = (smulLeft α ⋯) x
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ C a * X ^ (n + 1) = (monomial (n + 1)) a

Tactic:
rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.sum fun n a ↦ C a * X ^ n) = p

Tactic:
by
  simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n i : ℕ
h : i ≠ n
⊢ (erase n p).coeff i = p.coeff i

Tactic:
simp [coeff_erase, h]

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

Goal state before:
pp: R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) (a - b) = (monomial n) a - (monomial n) b

Tactic:
by
  rw [sub_eq_add_neg, map_add, monomial_neg, sub_eq_add_neg]

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

Goal state before:
pp: case inr
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
⊢ (lcomapDomain u hu) (Finsupp.basisSingleOne (v i)) = 0

Tactic:
ext j

Goal state after:
case inr
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : β
j : α
⊢ ((lcomapDomain u hu) (Finsupp.basisSingleOne (v i))) j = 0 j
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case inr.intro.intro
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2

Tactic:
constructor <;> refine UniqueMul.of_mulHom_image f hf
      ((UniqueMul.iff_card_le_one ?_ ?_).mpr <| (card_filter_le _ _).trans hc')

Goal state after:
case inr.intro.intro.left.refine_1
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p1.1 ∈ image (⇑f) A

case inr.intro.intro.left.refine_2
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p1.2 ∈ image (⇑f) B

case inr.intro.intro.right.refine_1
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p2.1 ∈ image (⇑f) A

case inr.intro.intro.right.refine_2
G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : TwoUniqueProds G
A B : Finset H
hc : 1 < #(A ×ˢ B)
hc' : #(image (⇑f) A ×ˢ image (⇑f) B) ≤ 1
p1 : H × H
h1 : p1 ∈ ↑(A ×ˢ B)
p2 : H × H
h2 : p2 ∈ ↑(A ×ˢ B)
hne : p1 ≠ p2
left✝¹ : p1.1 ∈ A
right✝¹ : p1.2 ∈ B
left✝ : p2.1 ∈ A
right✝ : p2.2 ∈ B
⊢ f p2.2 ∈ image (⇑f) B
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝¹ x✝ : M
⊢ mapRange.linearMap (id.flip (x✝¹ + x✝)) = mapRange.linearMap (id.flip x✝¹) + mapRange.linearMap (id.flip x✝)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
this :
  ∀ (M : Type u_1) (N : Type u_5) (α : Type (max u_3 u_4)) [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
    SMulCommClass N M α
x✝¹ : R
x✝ : M
⊢ mapRange.linearMap (id.flip (x✝¹ • x✝)) = (RingHom.id R) x✝¹ • mapRange.linearMap (id.flip x✝)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
S : Type u_5
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Module S N
inst✝¹ : SMulCommClass R S N
inst✝ : Finite ι
x : M →ₗ[R] ι →₀ N
⊢ (finsuppLinearMap S) (equivFunOnFinite.symm fun i ↦ lapply i ∘ₗ x) = x

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
| x ∈ q

Tactic:
← (prodEquivOfIsCompl p q h).apply_symm_apply x

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
| (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ q
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
| x ∈ p

Tactic:
← (prodEquivOfIsCompl p q h).apply_symm_apply x

Goal state after:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
| (p.prodEquivOfIsCompl q h) ((p.prodEquivOfIsCompl q h).symm x) ∈ p
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
⊢ p.liftQ (q.projectionOnto p ⋯) ⋯ ∘ₗ p.mkQ ∘ₗ q.subtype = LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
p q : Submodule R E
M : Type u_6
inst✝¹ : AddCommMonoid M
h : IsCompl p q
inst✝ : Module R M
f : M →ₗ[R] ↥p
⊢ p.projectionOnto q h ∘ₗ p.subtype ∘ₗ f = f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
p : Submodule R E
M : Type u_6
inst✝¹ : AddCommMonoid M
h✝ : IsComplemented p
inst✝ : Module R M
q : Submodule R E
h : IsCompl p q
f : ↥p →ₗ[R] M
⊢ (fun f ↦ f ∘ₗ p.subtype) (f ∘ₗ p.projectionOnto q h) = f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g ≤ ⨆ i, f i + g i

Tactic:
refine iSup_add_iSup_le fun i j => ?_

Goal state after:
case inr
ι : Sort u_2
f g : ι → ℕ∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j : ι
⊢ f i + g j ≤ ⨆ i, f i + g i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q w : RelSeries r
hpq : (p.last, q.head) ∈ r
hqw : (q.last, w.head) ∈ r
⊢ (p.append q hpq).append w ⋯ = p.append (q.append w hqw) ⋯

Tactic:
by
  ext
  · simp only [append_length, Nat.add_left_inj]
    lia
  · simp [append, Fin.append_assoc]

Goal state after:
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹⁰ : Monoid R
inst✝⁹ : Monoid S
inst✝⁸ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : DistribMulAction R A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : DistribMulAction S B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝¹ : NonUnitalNonAssocSemiring B₁
inst✝ : DistribMulAction R B₁
f : A →ₛₙₐ[φ] B
g : B → A
k : Function.RightInverse ⇑φ' ⇑φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
⊢ ((↑f).inverse g h₁ h₂).toFun 0 = 0

Tactic:
simp only [MulHom.toFun_eq_coe, MulHom.inverse_apply]
      rw [← f.map_zero, h₁]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
h : ↑n < height x
⊢ ∃ y < x, height y = ↑n

Tactic:
obtain ⟨m, hx : height x = m⟩ := Option.ne_none_iff_exists'.mp hfin.ne_top
    rw [hx] at h; norm_cast at h
    obtain ⟨p, hp, hlen⟩ := exists_series_of_height_eq_coe x hx
    use p ⟨n, by lia⟩
    constructor
    · rw [← hp]
      apply LTSeries.strictMono
      simp [Fin.last]; lia
    · exact height_eq_index_of_length_eq_height_last (by simp [hlen, hp, hx]) ⟨n, by lia⟩

Goal state after:
Module: Mathlib.Algebra.Algebra.Bilinear

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ toSpanSingleton R A 1 = Algebra.linearMap R A

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹¹ : IdemSemiring α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f (a + b) = f (a ⊔ b)

Tactic:
by rw [sup, add, add_eq_sup]

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m ∈ ⊥
n : R
x✝ : n ∈ S
⊢ m * n ∈ ⊥

Tactic:
rw [AddSubmonoid.mem_bot] at hm ⊢

Goal state after:
R : Type u_2
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ m * n = 0
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ (a * x + b * z) * (c * y + d * z) = 1

Tactic:
h1,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : IsCoprime y z
a b : R
h1 : a * x + b * z = 1
c d : R
h2 : c * y + d * z = 1
⊢ 1 * (c * y + d * z) = 1
Module: Mathlib.Algebra.Algebra.Operations

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
M : Submodule R A
⊢ span R ((fun x ↦ a * x) '' ↑M) = map (LinearMap.mulLeft R a) M

Tactic:
exact (map (LinearMap.mulLeft R a) M).span_eq

Goal state after: