mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Factorization.Defs

Goal state before:
pp: n p : ℕ
hp : Prime p
⊢ (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList

Tactic:
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]

Goal state after:
n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ n = p ^ k

Tactic:
← Nat.prod_factorization_pow_eq_self hn,

Goal state after:
n p k : ℕ
hn : n ≠ 0
h : n.factorization = single p k
⊢ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = p ^ k
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: n p b : ℕ
hb : n ≤ p ^ b
hn : ¬n = 0
⊢ n.factorization p ≤ b

Tactic:
if pp : p.Prime then
    exact (Nat.pow_le_pow_iff_right pp.one_lt).1 ((ordProj_le p hn).trans hb)
  else
    simp [factorization_eq_zero_of_not_prime n pp]

Goal state after:
Module: Mathlib.GroupTheory.OrderOfElement

Goal state before:
pp: G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a)).Finite

Tactic:
by
  classical rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _

Goal state after:
Module: Mathlib.Data.Nat.Choose.Factorization

Goal state before:
pp: p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ (n + 1).factorization p ≤ ((n + 1).choose (k + 1)).factorization p + (k + 1).factorization p

Tactic:
rw [← Pi.add_apply, ← coe_add, ← factorization_mul (ne_of_gt <| choose_pos hkn)
      (zero_ne_add_one k).symm]

Goal state after:
p n k : ℕ
hkn : k + 1 ≤ n + 1
hk : k + 1 ≠ 0
⊢ (n + 1).factorization p ≤ ((n + 1).choose (k + 1) * (k + 1)).factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: case inl
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : ¬Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

pp: case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p

Tactic:
· simp [pp]

Goal state after:
case inr
a b : ℕ
hb0 : b ≠ 0
hab : a ∣ b
p : ℕ
pp : Prime p
⊢ p ^ a.factorization p ∣ p ^ b.factorization p
Module: Mathlib.Data.Nat.Factorization.Basic

Goal state before:
pp: a b : ℕ
⊢ (∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p) ↔ a ∣ b

Tactic:
refine ⟨fun h => ?_, fun hab p => ordCompl_dvd_ordCompl_of_dvd hab p⟩

Goal state after:
a b : ℕ
h : ∀ (p : ℕ), a / p ^ a.factorization p ∣ b / p ^ b.factorization p
⊢ a ∣ b
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : 0 < p.degree
hmp : p.Monic
hq : q ≠ 0
zn0 : 0 ≠ 1
x✝ : p ^ (q.natDegree + 1) ∣ q
r : R[X]
hr : q = p ^ (q.natDegree + 1) * r
hp0 : p ≠ 0
hr0 : r ≠ 0
hpn1 : p.leadingCoeff ^ (q.natDegree + 1) = 1
hpn0' : p.leadingCoeff ^ (q.natDegree + 1) ≠ 0
⊢ (p ^ (q.natDegree + 1)).leadingCoeff * r.leadingCoeff ≠ 0

Tactic:
simp only [leadingCoeff_pow' hpn0', leadingCoeff_eq_zero, hpn1, one_mul, Ne,
          hr0, not_false_eq_true]

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

Goal state before:
pp: case pos.inl
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree < q.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
(modByMonic_eq_self_iff hq).mpr ‹_›

Goal state after:
case pos.inl
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree < q.degree
⊢ p.degree ≤ p.degree
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] (C a * p) = C a * (⇑derivative)^[k] p

Tactic:
simp_rw [← smul_eq_C_mul, iterate_derivative_smul]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Ring R
p q : R[X]
inst✝ : Ring S
f : R →+* S
hq : q.Monic
a✝ : Nontrivial S
this✝ : Nontrivial R
this : map f p /ₘ map f q = map f (p /ₘ q) ∧ map f p %ₘ map f q = map f (p %ₘ q)
⊢ map f (p /ₘ q) = map f p /ₘ map f q ∧ map f (p %ₘ q) = map f p %ₘ map f q

Tactic:
exact ⟨this.1.symm, this.2.symm⟩

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

Goal state before:
pp: case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k ∈ range n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)

Tactic:
mem_range

Goal state after:
case succ.e_a.refine_1
R : Type u
inst✝ : Semiring R
p q : R[X]
n : ℕ
IH : (⇑derivative)^[n] (p * q) = ∑ k ∈ range n.succ, n.choose k • ((⇑derivative)^[n - k] p * (⇑derivative)^[k] q)
k : ℕ
hk : k < n
⊢ n.choose (k + 1) • ((⇑derivative)^[n - (k + 1) + 1] p * (⇑derivative)^[k + 1] q) =
    n.choose k.succ • ((⇑derivative)^[n - k] p * (⇑derivative)^[k + 1] q)
Module: Mathlib.Algebra.Polynomial.Div

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst✝ : DecidablePred fun n ↦ ¬(X - C a) ^ (n + 1) ∣ p
⊢ (if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯

Tactic:
rw [dif_neg p0]

Goal state after:
R : Type u
inst✝¹ : Ring R
p : R[X]
p0 : p ≠ 0
a : R
inst✝ : DecidablePred fun n ↦ ¬(X - C a) ^ (n + 1) ∣ p
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.Order.Filter.Bases.Finite

Goal state before:
pp: α : Type u_1
s : Set (Set α)
⊢ generate s = generate (sInter '' {t | t.Finite ∧ t ⊆ s})

Tactic:
← FilterBasis.ofSets_sets,

Goal state after:
α : Type u_1
s : Set (Set α)
⊢ generate s = generate (FilterBasis.ofSets s).sets
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
s : Set ((i : ι) → α i)
I : Set ι
If : I.Finite
t : (i : ι) → Set (α i)
htf : ∀ (i : ι), t i ∈ f i
hts : I.pi t ⊆ s
⊢ s ∈ pi f

Tactic:
exact mem_of_superset (pi_mem_pi If fun i _ => htf i) hts

Goal state after:
Module: Mathlib.Order.Filter.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → Filter (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ (Filter.coprodᵢ f).NeBot ↔ ∃ d, (f d).NeBot

Tactic:
by
  simp [coprodᵢ_neBot_iff', *]

Goal state after:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Filter β
h : Filter γ
⊢ map (⇑(Equiv.prodAssoc α β γ)) ((f ×ˢ g) ×ˢ h) = f ×ˢ g ×ˢ h

Tactic:
by
  simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
    Function.comp_def, Equiv.prodAssoc_symm_apply]

Goal state after:
Module: Mathlib.Order.Filter.TendstoCofinite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ ↑y.support ⊆ range ⇑e

Tactic:
suffices y.support ⊆ s by simpa [e]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
f : α → β
inst✝ : TendstoCofinite f
x : β →₀ ℕ
s : Finset α := x.support.sup fun t ↦ ⋯.toFinset
e : ↥s ↪ α := Function.Embedding.subtype fun u ↦ u ∈ s
y : α →₀ ℕ
hy : mapDomain f y = x
⊢ y.support ⊆ s
Module: Mathlib.Algebra.BigOperators.Associated

Goal state before:
pp: M₀ : Type u_3
inst✝² : CommMonoidWithZero M₀
inst✝¹ : IsCancelMulZero M₀
inst✝ : Subsingleton M₀ˣ
s : Finset M₀
n : M₀
h : ∀ a ∈ s, Prime a
div : ∀ a ∈ s, a ∣ n
⊢ ∀ a ∈ Multiset.map (fun p ↦ p) s.val, Prime a

Tactic:
by simpa only [Multiset.map_id', Finset.mem_def] using h

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a x : R
⊢ p - C a ≠ 0 ∧ eval x (p - C a) = 0 ↔ p ≠ C a ∧ eval x p = a

Tactic:
sub_ne_zero,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a x : R
⊢ p ≠ C a ∧ eval x (p - C a) = 0 ↔ p ≠ C a ∧ eval x p = a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ Rel Associated (factors a) (factors b)

Tactic:
rcases iff_iff_and_or_not_and_not.mp h.eq_zero_iff with (⟨rfl, rfl⟩ | ⟨ha, hb⟩)
  · simp
  · refine factors_unique irreducible_of_factor irreducible_of_factor ?_
    exact ((factors_prod ha).trans h).trans (factors_prod hb).symm

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ t.prod ~ᵤ s.prod

Tactic:
have eq' : (Quot.mk Setoid.r : α → Associates α) = Associates.mk := funext quot_mk_eq_mk

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h : ⇑Associates.mkMonoidHom ∘ Classical.choose ⋯ = id
⊢ (map (⇑Associates.mkMonoidHom) (map (Classical.choose ⋯) (normalizedFactors x))).prod = x

Tactic:
map_map,

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
x : Associates α
hx : ¬x = 0
h : ⇑Associates.mkMonoidHom ∘ Classical.choose ⋯ = id
⊢ (map (⇑Associates.mkMonoidHom ∘ Classical.choose ⋯) (normalizedFactors x)).prod = x
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map (algebraMap S R) (map (algebraMap T S) p)).roots = (map (algebraMap T R) p).roots

Tactic:
map_map,

Goal state after:
R : Type u
S : Type v
T : Type w
inst✝⁷ : CommRing R
inst✝⁶ : IsDomain R
inst✝⁵ : CommRing T
p : T[X]
inst✝⁴ : CommRing S
inst✝³ : Algebra T S
inst✝² : Algebra S R
inst✝¹ : Algebra T R
inst✝ : IsScalarTower T S R
⊢ (map ((algebraMap S R).comp (algebraMap T S)) p).roots = (map (algebraMap T R) p).roots
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x✝ : R
⊢ x✝ ∈ image f univ → x✝ ∈ p.roots.toFinset

Tactic:
simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
    IsRoot.def, forall_exists_index, hp, not_false_eq_true]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : R[X]
ι : Type u_2
inst✝ : Fintype ι
f : ι → R
hf : Function.Injective f
heval : ∀ (i : ι), eval (f i) p = 0
hcard : p.natDegree < Fintype.card ι
hp : ¬p = 0
x✝ : R
⊢ ∀ (x : ι), f x = x✝ → eval x✝ p = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b •
      (m.descFactorial (m - b) • eval t (X - C t) ^ (m - (m - b)) * eval t ((⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) =
    0

Tactic:
Nat.sub_sub_self (mem_range_succ_iff.mp hb),

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
m : ℕ := rootMultiplicity t p
hm : m = rootMultiplicity t p
b : ℕ
hb : b ∈ range m.succ
hb0 : b ≠ 0
⊢ m.choose b • (m.descFactorial (m - b) • eval t (X - C t) ^ b * eval t ((⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ p ∈ ↑l ↔ ⟨p, hp⟩ ∈ l

Tactic:
dsimp only [Membership.mem]; dsimp only [FactorSetMem]; split_ifs; rfl

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

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

Tactic:
rcases Associates.mk_surjective a with ⟨a, rfl⟩

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ (Associates.mk a).factors.prod = Associates.mk a
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ IsUnit (p * q).content

Tactic:
refine (associated_content_mul p q).symm.isUnit ?_

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
⊢ IsUnit (p.content * q.content)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C (p * q).content * (p * q).primPart

Tactic:
rw [← (p * q).eq_C_content_mul_primPart,
    p.eq_C_content_mul_primPart, q.eq_C_content_mul_primPart, mul_mul_mul_comm, ← C_mul]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C (p.content * q.content) * (p.primPart * q.primPart)
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C (p * q).content * (p.primPart * q.primPart)

Tactic:
content_mul,

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
⊢ C p.content * p.primPart * (C q.content * q.primPart) = C (p.content * q.content) * (p.primPart * q.primPart)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ (X ^ n).rootSet S = {0}

Tactic:
← one_mul (X ^ n : R[X]),

Goal state after:
R : Type u
S : Type v
inst✝³ : Field R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
n : ℕ
hn : n ≠ 0
⊢ (1 * X ^ n).rootSet S = {0}
Module: Mathlib.RingTheory.Polynomial.UniqueFactorization

Goal state before:
pp: case pos
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f a : R[X]
ane0 : a ≠ 0
c : R[X]
not_unit_c : ¬IsUnit c
hac : a * c = 0
⊢ ↑a.degree < ⊤

Tactic:
exact WithTop.coe_lt_top _

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

Goal state before:
pp: R : Type u
inst✝ : Field R
p : R[X]
hp0 : p ≠ 0
hpu : ¬IsUnit p
⊢ Irreducible p ↔ ∀ (q : R[X]), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Tactic:
by
  have : p * C (leadingCoeff p)⁻¹ ≠ 1 := by
    contrapose hpu
    exact .of_mul_eq_one _ hpu
  rw [← irreducible_mul_leadingCoeff_inv,
      (monic_mul_leadingCoeff_inv hp0).irreducible_iff_lt_natDegree_lt this,
      natDegree_mul_leadingCoeff_inv _ hp0]
  simp only [IsUnit.dvd_mul_right
    (isUnit_C.mpr (IsUnit.mk0 (leadingCoeff p)⁻¹ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))]

Goal state after:
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
h : P → N
hgh : RightInverse h ⇑g
⊢ inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g = (rTensor Q f).range.mkQ

Tactic:
rw [LinearMap.ext_iff]
  intro y
  simp only [coe_comp, Function.comp_apply, Submodule.mkQ_apply,
    rTensor.inverse_of_rightInverse_apply]

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

Goal state before:
pp: case tmul
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
x : M
y : N
⊢ ∃ k m n, x ⊗ₜ[R] y = ∑ j, m j ⊗ₜ[R] n j

Tactic:
exact ⟨1, fun _ ↦ x, fun _ ↦ y, by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FGBaseChange

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ ∃ C, C.FG ∧ x ∈ Subalgebra.baseChange A C

Tactic:
classical
  refine ⟨Algebra.adjoin R (S.image fun j ↦ j.2), ?_, ?_⟩
  · exact Subalgebra.fg_adjoin_finset _
  · exact hS ▸ Subalgebra.sum_mem _ fun s hs ↦ (Subalgebra.tmul_mem_baseChange
      (Algebra.subset_adjoin (Finset.mem_image_of_mem _ hs)) s.1)

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective (⇑↑(LinearEquiv.rTensor M e) ∘ ⇑(rTensor M f)) ↔
    Injective (⇑(rTensor M (↑e ∘ₗ f).range.subtype) ∘ ⇑↑(LinearEquiv.rTensor M (LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯)))

Tactic:
← coe_comp,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : N →ₗ[R] P
hf : Injective ⇑f
e : P ≃ₗ[R] Q
⊢ Injective ⇑(↑(LinearEquiv.rTensor M e) ∘ₗ rTensor M f) ↔
    Injective ⇑(rTensor M (↑e ∘ₗ f).range.subtype ∘ₗ ↑(LinearEquiv.rTensor M (LinearEquiv.ofInjective (↑e ∘ₗ f) ⋯)))
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective (⇑(lTensor P i) ∘ ⇑(rTensor N Q.subtype))

Tactic:
← coe_comp,

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective ⇑(lTensor P i ∘ₗ rTensor N Q.subtype)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective (⇑↑(directSumRight R R P M) ∘ ⇑(rTensor (⨁ (i : ι), M i) N.subtype))) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)

Tactic:
← coe_comp,

Goal state after:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(↑(directSumRight R R P M) ∘ₗ rTensor (⨁ (i : ι), M i) N.subtype)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Injective ⇑(rTensor (M i) N.subtype)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s \ t ∪ t).dens = (s ∪ t).dens

Tactic:
sdiff_union_self_eq_union

Goal state after:
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∪ t).dens = (s ∪ t).dens
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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x⟩⟧ ^ Int.negSucc n = map f f (fun x x_1 ↦ x_1⁻¹) ⋯ (⟦⟨i, x⟩⟧ ^ ↑n.succ)

Tactic:
simp_rw [HPow.hPow, Pow.pow, map_def]

Goal state after:
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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x ^ Int.negSucc n⟩⟧ = ⟦⟨i, (x ^ ↑n.succ)⁻¹⟩⟧
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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x⟩⟧ ^ Int.negSucc n = map f f (fun x x_1 ↦ x_1⁻¹) ⋯ (⟦⟨i, x⟩⟧ ^ ↑n.succ)

Tactic:
simp_rw [HPow.hPow, Pow.pow, map_def]

Goal state after:
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✝⁴ : Nonempty ι
inst✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
n : ℕ
i : ι
x : G i
⊢ ⟦⟨i, x ^ Int.negSucc n⟩⟧ = ⟦⟨i, (x ^ ↑n.succ)⁻¹⟩⟧