mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f ×ˢ g = map Prod.swap (g ×ˢ f)

Tactic:
by
  rw [prod_comm', ← map_swap_eq_comap_swap]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p r : α
h : ∀ {m : α}, m ∈ normalizedFactors r → m = p
hr : r ≠ 0
⊢ ∃ i, p ^ i ~ᵤ r

Tactic:
use (normalizedFactors r).card
  have := UniqueFactorizationMonoid.prod_normalizedFactors hr
  rwa [Multiset.eq_replicate_of_mem fun b => h, Multiset.prod_replicate] at this

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
x : Associates α
hx : x ∈ p + factors c
⊢ Irreducible x

pp: case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod

Tactic:
· obtain h | h := Multiset.mem_add.1 hx
    · exact hp x h
    · exact irreducible_of_factor _ h

Goal state after:
case refine_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ a ∈ p, Irreducible a
hq : ∀ a ∈ q, Irreducible a
c : Associates α
eqc : q.prod = p.prod * c
⊢ q.prod = (p + factors c).prod
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ~ᵤ (Classical.choose ⋯).prod

Tactic:
apply (Classical.choose_spec (pf _ _)).2.symm

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ≠ 0
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: T : Type w
inst✝⁵ : CommRing T
p : T[X]
S : Type u_1
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : S
⊢ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0 ↔ p ≠ 0 ∧ (aeval a) p = 0

Tactic:
Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective T S)

Goal state after:
T : Type w
inst✝⁵ : CommRing T
p : T[X]
S : Type u_1
inst✝⁴ : IsDomain T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : Module.IsTorsionFree T S
a : S
⊢ p ≠ 0 ∧ (aeval a) p = 0 ↔ p ≠ 0 ∧ (aeval a) p = 0
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
h : p ≠ 0
n : ℕ
ih : (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → ↑n ! ∈ nonZeroDivisors R
hnzd : ∀ m ≤ n + 1, m ≠ 0 → ↑m ∈ nonZeroDivisors R
⊢ ↑(n + 1)! ∈ nonZeroDivisors R

Tactic:
rw [Nat.factorial_succ, Nat.cast_mul, mul_mem_nonZeroDivisors]
    exact ⟨hnzd _ le_rfl n.succ_ne_zero, ih fun m h ↦ hnzd m (h.trans n.le_succ)⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
h : (q.primPart * p.primPart).content = 1
⊢ Associated (C p.content * p.primPart * (C q.content * q.primPart)).content
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)

Tactic:
by
      grw [mul_assoc, associated_content_C_mul, associated_content_C_mul, mul_comm p.primPart,
        mul_assoc, associated_content_C_mul, associated_content_C_mul, h, mul_one,
        content_primPart, content_primPart, mul_one, mul_one]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b

Tactic:
obtain ⟨⟨p0, p0_irr⟩, p0_mem⟩ := Multiset.exists_mem_of_ne_zero ((mt WithTop.coe_eq_coe.mpr) hz)

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : ⟨p0, p0_irr⟩ ∈ factors' a ⊓ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
by
  rw [← p.roots.card_map f]
  exact Multiset.card_le_card (map_roots_le h)

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ Associates.mk a ≤ Associates.mk b

Tactic:
mk_le_mk_iff_dvd

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ Associates.mk a ≤ Associates.mk b

Tactic:
mk_le_mk_iff_dvd

Goal state after:
α✝ : Type u_1
α : Type u_2
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : NormalizationMonoid α
a b c : α
hac : a ∣ c
hab : a ∣ b
⊢ a ∣ c ∧ a ∣ b
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ f ((aeval a) p) = 0

Tactic:
ha,

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
B : Type u_2
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
a : A
h : IsAlgebraic R a
p : R[X]
hp : p ≠ 0
ha : (aeval a) p = 0
⊢ f 0 = 0
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
n : ℕ
s : Set (σ →₀ ℕ)
⊢ restrictSupport R (n • s) = restrictSupport R s ^ n

Tactic:
by
  induction n <;> simp [add_smul, restrictSupport_add, *, pow_succ]

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

Goal state before:
pp: case zero
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, 0 = (Multiset.map (fun i ↦ i.1 ⊗ₜ[R] i.2) S).sum

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: case a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (span (⇑includeLeft '' ↑I)))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x

Tactic:
← submodule_span_eq

Goal state after:
case a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case zero
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, 0 = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
exact ⟨0, by simp⟩

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

Goal state before:
pp: case a.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
⊢ ∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = 0

Tactic:
use 0
      simp only [map_zero]

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

Goal state before:
pp: case a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (span (⇑includeRight '' ↑I)))
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x

Tactic:
← submodule_span_eq

Goal state after:
case a
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_2
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
⊢ ∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = 0

Tactic:
use 0
      simp only [map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
this : a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
⊢ ↑b ∈ I

Tactic:
exact Submodule.coe_mem b

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ ↑↑j.succ = ↑⟨j, hj⟩.succ

Tactic:
simp [hj]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : 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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
i : ι
⊢ (g ⟨?i, ↑q⟩.fst) ⟨?i, ↑q⟩.snd = ↑q

pp: case i
ι : 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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
i : ι
⊢ ι

Tactic:
map_ratCast (g i)

Goal state after:
ι : 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 : ι) → DivisionRing (G i)
inst✝² : DivisionRing C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), RingHomClass (H i) (G i) C
g : (i : ι) → H i
h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)
q : ℚ
i : ι
⊢ ↑q = ↑q
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
simp [hj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : j = k
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
simp [hj]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Tactic:
· simp only [hj₁]
    by_cases hk : 0 = k
    · simp only [natCast_zero, intervalGapsWithin_zero_fst]
      simp [show 0 = last k by grind, hab]
    · exact hFab (F.intervalGapsWithin_mapsTo h a b (x := 0) (by grind)) |>.left

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hab : a ≤ b
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hF : (↑F).PairwiseDisjoint fun z ↦ Icc z.1 z.2
j : ℕ
hj : j < k + 1
hj₁ : ¬j = 0
⊢ (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
x : N
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
⊢ (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun (r • x) =
    (RingHom.id S) r • (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun x

Tactic:
have hF : ∀ (s : S) (m : M), h.lift F (s • f m) = s • g m := h.lift_eq F

Goal state after:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : AddCommMonoid N
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : Module S N
inst✝⁶ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
x : N
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
⊢ (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun (r • x) =
    (RingHom.id S) r • (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun x
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b a : α
s : Finset α
ha : a ∉ s
⊢ Disjoint (map (Sym2.mkEmbedding a) (cons a s ha)) s.sym2

Tactic:
simp [Finset.disjoint_left, ha]

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

Goal state before:
pp: α : Type u_1
n : ℕ
xs✝ : List α
a : α
xs : List α
z : Sym α 0
ha : a ∈ z
hz : z ∈ List.sym 0 xs
⊢ a ∈ xs

Tactic:
cases Sym.eq_nil_of_card_zero z
    simp at ha

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

Goal state before:
pp: α : Type u_1
x y : α
⊢ ↑s(x, y) = {x, y}

Tactic:
ext z; simp

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

Goal state before:
pp: α : Type u_1
z : Sym2 α
⊢ z ∈ fromRel ⋯ ↔ z ∈ {z | ¬z.IsDiag}

Tactic:
exact z.ind (by simp)

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

Goal state before:
pp: case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp (Quiver.reverse (Quiver.reverse a✝)).toPath = a✝¹.cons a✝

Tactic:
Quiver.reverse_reverse

Goal state after:
case cons
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : a✝¹.reverse.reverse = a✝¹
⊢ a✝¹.comp a✝.toPath = a✝¹.cons a✝
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
    e.unitIso.hom.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)

Tactic:
rw [← e.unit_naturality]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
    e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y) ≫ e.unit.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

Tactic:
rw [← e.unit_naturality]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitIso.inv.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ Hom.left sq ≫ g.hom ≫ inv (Hom.right sq) = f.hom

Tactic:
simp only [← Category.assoc, IsIso.comp_inv_eq, w]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
hP : P.RespectsIso
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
h : P (f ≫ g)
⊢ P g

Tactic:
simpa using RespectsIso.precomp P (inv f) (f ≫ g) h

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ P.map E.inverse f

Tactic:
refine ⟨_, _, _, hf, ⟨?_⟩⟩

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ Arrow.mk (E.inverse.map (E.functor.map f)) ≅ Arrow.mk f
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).left = eqToHom ⋯

Tactic:
cases H
  rfl

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

Goal state before:
pp: A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).right = eqToHom ⋯

Tactic:
cases H
  rfl

Goal state after: