mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ f s ≤ ∑ x ∈ f.support, f x • w x

Tactic:
rw [h]

Goal state after:
case neg
σ : Type u_1
w : σ → ℕ
s : σ
hs : w s ≠ 0
f : σ →₀ ℕ
h : f s = 0
⊢ 0 ≤ ∑ x ∈ f.support, f x • w x
Module: Mathlib.Data.Finsupp.Weight

Goal state before:
pp: σ : Type u_1
R : Type u_5
inst✝ : Semiring R
⊢ degree = weight fun x ↦ 1

Tactic:
ext d
  simp [weight_apply, smul_eq_mul, mul_one]

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

Goal state before:
pp: σ : Type u_5
s t : Set ℕ
⊢ ⇑degree ⁻¹' (s + t) = ⇑degree ⁻¹' s + ⇑degree ⁻¹' t

Tactic:
refine (Set.preimage_add_preimage_subset ..).antisymm' ?_

Goal state after:
σ : Type u_5
s t : Set ℕ
⊢ ⇑degree ⁻¹' (s + t) ⊆ ⇑degree ⁻¹' s + ⇑degree ⁻¹' t
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : a * b = 0
ha0 : a = 0
⊢ p ∣ a ∨ p ∣ b

Tactic:
simp [ha0]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
⊢ p ∣ a ∨ p ∣ b

Tactic:
have hx0 : x ≠ 0 := fun hx0 => by simp_all

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
uif :
  ∀ (f g : Multiset α),
    (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
p : α
this : DecidableEq α := Classical.decEq α
hpi : Irreducible p
a b : α
x✝ : p ∣ a * b
x : α
hx : a * b = p * x
hab0 : ¬a * b = 0
hx0 : x ≠ 0
⊢ p ∣ a ∨ p ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x = normalizedFactors y
⊢ (normalizedFactors x).prod ~ᵤ (normalizedFactors y).prod

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
b : α
hbmem : b ∈ factors a
hab : a ~ᵤ b
⊢ ∃ b, a ~ᵤ b ∧ factors a = {b}

Tactic:
exact ⟨b, hab, .symm <| Multiset.eq_of_le_of_card_le (Multiset.singleton_le.mpr hbmem)
    (by rw [card_factors_of_irreducible ha, Multiset.card_singleton])⟩

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s✝ : Set α
s : Set (α →₀ ℕ)
⊢ ((fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' s) ^ n = (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' (n • s)

Tactic:
refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_

Goal state after:
α : Type u_5
β : Type u_6
inst✝ : CommMonoid β
f : α → β
n : ℕ
s✝ : Set α
s : Set (α →₀ ℕ)
⊢ ⇑{ toFun := (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) ∘ ⇑Multiplicative.toAdd, map_one' := ⋯, map_mul' := ⋯ } '' s ^ n =
    (fun x ↦ x.prod fun x1 x2 ↦ f x1 ^ x2) '' (n • s)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ p.coeff n

Tactic:
rw [h]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
h : p.coeff n = 0
⊢ p.content ∣ 0
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (X * p).support.val = Multiset.map p.coeff p.support.val

Tactic:
rw [h]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
h : (X * p).support = Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support
⊢ Multiset.map (X * p).coeff (Finset.map { toFun := Nat.succ, inj' := Nat.succ_injective } p.support).val =
    Multiset.map p.coeff p.support.val
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime p

Tactic:
obtain ⟨f, hf⟩ := pf p hp0

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ p
⊢ Prime p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h✝ : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
h : derivative p = 0
⊢ (X - C t) ^ m ∣ derivative p

Tactic:
rw [h]

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
h✝ : ¬p = 0
g : R[X]
hndvd✝ : ¬X - C t ∣ g
m : ℕ := rootMultiplicity t p
hnzd : ↑m ∈ nonZeroDivisors R
hp : p = (X - C t) ^ m * g
hm : m - 1 + 1 = m
hndvd : ¬(X - C t) ^ m ∣ derivative p
h : derivative p = 0
⊢ (X - C t) ^ m ∣ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Finite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : 0 ∣ y
hx : x = 0
⊢ y = 0

Tactic:
zero_dvd_iff

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : UniqueFactorizationMonoid M
inst✝ : Fintype Mˣ
y : M
hy : y ≠ 0
this✝² : Nontrivial M
this✝¹ : StrongNormalizationMonoid M
this✝ : DecidableEq M
this : DecidableEq (Associates M)
x : M
h : y = 0
hx : x = 0
⊢ y = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ factors' a = factors' 0

Tactic:
rw [h]

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

Goal state before:
pp: R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < q.degree

Tactic:
← degree_mul_leadingCoeff_inv q hq

Goal state after:
R : Type u
inst✝ : Field R
q p : R[X]
hq : q ≠ 0
⊢ (p.mod q).degree < (q * C q.leadingCoeff⁻¹).degree
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
h : a.factors = b.factors
⊢ a.factors.prod = b.factors.prod

Tactic:
rw [h]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ rootMultiplicity a p ≤ rootMultiplicity (f a) (map f p)

Tactic:
le_rootMultiplicity_iff hmap

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ (X - C (f a)) ^ rootMultiplicity a p ∣ map f p
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
h : p.degree = 1
⊢ p.degree ≤ 1

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
⊢ k ∣ p.count (a * b).factors

Tactic:
rw [h]

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
a✝ : Nontrivial α
hk0 : ¬k = 0
p : Associates α
hp : Irreducible p
⊢ k ∣ p.count (c ^ k).factors
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_ne : (aeval x) p.divX ≠ 0
⊢ x⁻¹ = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

Tactic:
rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]
  conv_lhs => rw [← divX_mul_X_add p]
  · rw [map_add, map_mul, aeval_X, aeval_C]
  · exact aeval_ne

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))

Tactic:
aeval_eq,

Goal state after:
case e'_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ -((aeval x) p.divX / (algebraMap K L) (p.coeff 0)) = (aeval x) p.divX / (0 - (algebraMap K L) (p.coeff 0))
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ ↑((aeval x) p) = 0

Tactic:
aeval_eq,

Goal state after:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ ↑0 = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
rw [x_eq, Subalgebra.coe_zero, inv_zero]

Goal state after:
case refine_3.inr
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0 ∈ A
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
inst✝¹ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝ : DecidableEq ι
⊢ ∀ (s : R) {m m' : DirectSum ι G}, Eqv f m m' → Eqv f (s • m) (s • m')

Tactic:
by rintro _ _ _ ⟨⟩; simpa only [← map_smul] using .of_map ..

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
y : Q ⊗[R] P
hy : ∃ a, (lTensor Q g) a = y
x : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + y

Tactic:
obtain ⟨y, rfl⟩ := hy

Goal state after:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : Q ⊗[R] N
⊢ ∃ a, (lTensor Q g) a = (lTensor Q g) x + (lTensor Q g) y
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
y : P ⊗[R] Q
hy : ∃ a, (rTensor Q g) a = y
x : N ⊗[R] Q
⊢ ∃ a, (rTensor Q g) a = (rTensor Q g) x + y

Tactic:
obtain ⟨y, rfl⟩ := hy

Goal state after:
case add
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
x y : N ⊗[R] Q
⊢ ∃ a, (rTensor Q g) a = (rTensor Q g) x + (rTensor Q g) y
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ P ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
← Subtype.coe_le_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑P ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ Q ≤ ⟨↑P ⊔ ↑Q, ⋯⟩

Tactic:
← Subtype.coe_le_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P Q : { P // Small.{u, u_2} ↥P }
⊢ ↑Q ≤ ↑⟨↑P ⊔ ↑Q, ⋯⟩
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ x✝ : { P // Small.{u, u_2} ↥P }
hPR : x✝² ≤ x✝
hQR : x✝¹ ≤ x✝
⊢ ⟨↑x✝² ⊔ ↑x✝¹, ⋯⟩ ≤ x✝

Tactic:
← Subtype.coe_le_coe

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝² x✝¹ x✝ : { P // Small.{u, u_2} ↥P }
hPR : ↑x✝² ≤ ↑x✝
hQR : ↑x✝¹ ≤ ↑x✝
⊢ ↑⟨↑x✝² ⊔ ↑x✝¹, ⋯⟩ ≤ ↑x✝
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
h : P → N
hgh : RightInverse h ⇑g
z : Q ⊗[R] P
⊢ (toFun Q hfg).toFun ((inverse_of_rightInverse Q hfg hgh) z) = z

Tactic:
by
    simp only [AddHom.toFun_eq_coe, coe_toAddHom]
    obtain ⟨y, rfl⟩ := lTensor_surjective Q (hgh.surjective) z
    rw [lTensor.inverse_of_rightInverse_apply]
    simp only [lTensor.toFun, Submodule.liftQ_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
ih : ∃ M' N', M'.FG ∧ N'.FG ∧ s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert a s ⊆ ↑(mapIncl M' N').range

Tactic:
obtain ⟨M', N', hM', hN', h⟩ := ih

Goal state after:
case insert
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert a s ⊆ ↑(mapIncl M' N').range
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁸ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁷ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁶ : (i : ι) → FunLike (H i) (G i) C
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → Mul (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝¹ : (i : ι) → StarMul (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x✝¹ x✝ : G i
⊢ star (⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧) = star ⟦⟨i, x✝⟩⟧ * star ⟦⟨i, x✝¹⟩⟧

Tactic:
by simp_rw [mul_def, star_def, star_mul, mul_def]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : s ∩ t = ∅
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

pp: case inr
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : (s ∩ t).Nonempty
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i

Tactic:
· simp [expect, hst]

Goal state after:
case inr
ι : Type u_1
M : Type u_4
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → M
hst : (s ∩ t).Nonempty
⊢ (𝔼 i ∈ s, if i ∈ t then f i else 0) = (↑(#(s ∩ t)) / ↑(#s)) • 𝔼 i ∈ s ∩ t, f i
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ lift (mk R M N) = LinearMap.id

Tactic:
apply TensorProduct.ext'
    simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
x✝ : M₁
y✝ : M₂
⊢ motive ((f x✝) y✝)

Tactic:
apply tmul

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inr.refine_1
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ n ≤ i + a * (n / a)

Tactic:
exact hn.symm.le.trans (add_le_add_left hi _)

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: n a : ℤ
h : 0 ≤ a
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = Ico 0 a

Tactic:
obtain rfl | ha := eq_or_lt_of_le h
  · simp
  ext i
  simp only [mem_image, mem_Ico]
  constructor
  · rintro ⟨i, _, rfl⟩
    exact ⟨emod_nonneg i ha.ne', emod_lt_of_pos i ha⟩
  rintro ⟨hi₀, hia⟩
  have hn := Int.emod_add_mul_ediv n a
  obtain hi | hi := lt_or_ge i (n % a)
  · refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · calc
        n = 0 + n % a + a * (n / a) := by simp [hn]
        _ ≤ i + a + a * (n / a) := by gcongr; exact (Int.emod_lt_of_pos n ha).le
        _ = i + a * (n / a + 1) := by grind
    · calc
        i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]
  · refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · exact hn.symm.le.trans (add_le_add_left hi _)
    · rw [add_comm n a]
      refine add_lt_add_of_lt_of_le hia (le_trans ?_ hn.le)
      simp only [le_add_iff_nonneg_left]
      exact Int.emod_nonneg n (ne_of_gt ha)
    · rw [Int.add_mul_emod_self_left, Int.emod_eq_of_lt hi₀ hia]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
by
  rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]

Goal state after:
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (s(x, x) :: (map (fun y ↦ s(x, y)) xs ++ xs.sym2)).dedup = (x :: xs).dedup.sym2

Tactic:
· rw [dedup_cons_of_notMem hm, List.sym2, map_cons, ← ih, dedup_cons_of_notMem, cons_append,
        List.Disjoint.dedup_append, dedup_map_of_injective]
      · exact (Sym2.mkEmbedding _).injective
      · exact map_mk_disjoint_sym2 x xs hm
      · simp [hm, mem_sym2_iff]

Goal state after:
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: case h
α : Type u_1
inst✝ : LinearOrder α
t : Sym2 α
a b : α
⊢ s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t

Tactic:
| _ a b
   => 

Goal state after:
case h
α : Type u_1
inst✝ : LinearOrder α
t : Sym2 α
a b : α
⊢ s(a, b).inf = t.inf ∧ s(a, b).sup = t.sup ↔ s(a, b) = t
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ IsBaseChange R ↑e

Tactic:
apply IsBaseChange.of_lift_unique
  intro Q I₁ I₂ I₃ I₄ g
  have : I₂ = I₃ := by
    ext r q
    change (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
    dsimp
    rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
  cases this
  refine
    ⟨g.comp e.symm.toLinearMap, by
      ext
      simp, ?_⟩
  rintro y (rfl : _ = _)
  ext
  simp

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
e : Sym2 α
⊢ e = s((Quot.out e).1, (Quot.out e).2)

Tactic:
rw [Sym2.mk, e.out_eq]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
⊢ homOfEq f hX hY ≍ g ↔ f ≍ g

Tactic:
cases hX

Goal state after:
case refl
V : Type u_1
inst✝ : Quiver V
X Y Y' : V
f : X ⟶ Y
hY : Y = Y'
g : X ⟶ Y'
⊢ homOfEq f ⋯ hY ≍ g ↔ f ≍ g
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
g : X' ⟶ Y'
hX : X' = X
hY : Y' = Y
⊢ f ≍ homOfEq g hX hY ↔ f ≍ g

Tactic:
cases hX

Goal state after:
case refl
V : Type u_1
inst✝ : Quiver V
X Y Y' : V
f : X ⟶ Y
hY : Y' = Y
g : X ⟶ Y'
⊢ f ≍ homOfEq g ⋯ hY ↔ f ≍ g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
exfalso
          simp at hx

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Category

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : F ⟶ G
h : α = β
X : C
⊢ α.app X = β.app X

Tactic:
rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g

Tactic:
rw [h]

Goal state after: