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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
p : ι → Prop
s : ι → Set α
t : Set α
⊢ t ∈ ⨅ i, ⨅ (_ : p i), 𝓟 (s i) → ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t

Tactic:
simp only [mem_iInf (ι := ι), mem_iInf_of_finite, mem_principal]
    rintro ⟨I, hIf, V, hV₁, hV₂, rfl⟩
    choose! t ht₁ ht₂ using hV₁
    refine ⟨I ∩ {i | p i}, hIf.inter_of_left _, fun i ↦ And.right, ?_⟩
    simp only [mem_inter_iff, iInter_and, biInter_eq_iInter, ht₂, mem_ofPred_eq]
    gcongr with i hpi
    exact ht₁ i hpi

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ x, f (Equiv.plift x)).sets = (⨅ i, f i.down).sets

Tactic:
Equiv.plift_apply

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨅ x, f x.down).sets = (⨅ i, f i.down).sets
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ derivative (C r) = eval₂ C q (derivative (C r)) * derivative q

Tactic:
derivative_C,

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
r : R
⊢ 0 = eval₂ C q 0 * derivative q
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s \ t) = cofinite ⊓ 𝓟 s

Tactic:
sdiff_eq,

Goal state after:
α : Type u_2
s t : Set α
ht : t.Finite
⊢ cofinite ⊓ 𝓟 (s ∩ tᶜ) = cofinite ⊓ 𝓟 s
Module: Mathlib.Order.Filter.Cofinite

Goal state before:
pp: ⊢ cofinite ≤ atTop

Tactic:
refine atTop_basis.ge_iff.2 fun N _ => ?_

Goal state after:
N : ℕ
x✝ : True
⊢ Ici N ∈ cofinite
Module: Mathlib.Algebra.Polynomial.Derivative

Goal state before:
pp: R : Type u
inst✝ : Ring R
c : R
⊢ 1 - derivative (C c) = 1

Tactic:
derivative_C,

Goal state after:
R : Type u
inst✝ : Ring R
c : R
⊢ 1 - 0 = 1
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r * GCDMonoid.gcd p q / GCDMonoid.gcd p q ≠ 0

Tactic:
mul_div_cancel_right₀ _ pq0

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hp : p ≠ 0
r : R
hr : p = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.EuclideanDomain

Goal state before:
pp: R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r * GCDMonoid.gcd p q / GCDMonoid.gcd p q ≠ 0

Tactic:
mul_div_cancel_right₀ _ pq0

Goal state after:
R : Type u_1
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
p q : R
hq : q ≠ 0
r : R
hr : q = GCDMonoid.gcd p q * r
pq0 : GCDMonoid.gcd p q ≠ 0
r0 : r ≠ 0
⊢ r ≠ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case e'_2
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ p = normalize p

Tactic:
apply (normalize_normalized_factor _ ‹_›).symm

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

Goal state before:
pp: case e'_3
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
hp : p ∈ normalizedFactors a
q : α
hq : q ∈ normalizedFactors a
hdvd : p ∣ q
⊢ q = normalize q

Tactic:
apply (normalize_normalized_factor _ ‹_›).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ normalizedFactors b).prod

Tactic:
rw [Multiset.prod_cons]
            exact (prod_normalizedFactors hb0).symm.mul_left _

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 b : R
ha : IsUnit a
⊢ (p.comp (C a * X + C b)).roots = Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) p.roots

Tactic:
conv_rhs => rw [← p.map_roots_comp_C_mul_X_add_C a b ha]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
a b : R
ha : IsUnit a
⊢ (p.comp (C a * X + C b)).roots =
    Multiset.map (fun x ↦ a⁻¹ʳ * (x - b)) (Multiset.map (fun x ↦ a * x + b) (p.comp (C a * X + C b)).roots)
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
        have ha0 : a ≠ 0 := left_ne_zero_of_mul hab0
        have hb0 : b ≠ 0 := right_ne_zero_of_mul hab0
        obtain ⟨fx, hfx⟩ := eif x hx0
        obtain ⟨fa, hfa⟩ := eif a ha0
        obtain ⟨fb, hfb⟩ := eif b hb0
        have h : Multiset.Rel Associated (p ::ₘ fx) (fa + fb) := by
          apply uif
          · exact fun i hi => (Multiset.mem_cons.1 hi).elim (fun hip => hip.symm ▸ hpi) (hfx.1 _)
          · exact fun i hi => (Multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _)
          calc
            Multiset.prod (p ::ₘ fx) ~ᵤ a * b := by
              rw [hx, Multiset.prod_cons]; exact hfx.2.mul_left _
            _ ~ᵤ fa.prod * fb.prod := hfa.2.symm.mul_mul hfb.2.symm
            _ = _ := by rw [Multiset.prod_add]
        exact
          let ⟨q, hqf, hq⟩ := Multiset.exists_mem_of_rel_of_mem h (Multiset.mem_cons_self p _)
          (Multiset.mem_add.1 hqf).elim
            (fun hqa =>
              Or.inl <| hq.dvd_iff_dvd_left.2 <| hfa.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqa))
            fun hqb =>
            Or.inr <| hq.dvd_iff_dvd_left.2 <| hfb.2.dvd_iff_dvd_right.1 (Multiset.dvd_prod hqb)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ Function.RightInverse
    (⇑{ toFun := fun a ↦ if a = 0 then 0 else (map (Classical.choose ⋯) (normalizedFactors a)).prod, map_one' := ⋯,
        map_mul' := ⋯ })
    Associates.mk

Tactic:
by
      intro x
      dsimp
      by_cases hx : x = 0
      · simp [hx]
      have h : Associates.mkMonoidHom ∘ Classical.choose mk_surjective.hasRightInverse =
          (id : Associates α → Associates α) := by
        ext x
        rw [Function.comp_apply, mkMonoidHom_apply,
          Classical.choose_spec mk_surjective.hasRightInverse x]
        rfl
      rw [if_neg hx, ← mkMonoidHom_apply, MonoidHom.map_multiset_prod, map_map, h, map_id, ←
        associated_iff_eq]
      apply prod_normalizedFactors hx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : DecidableEq S
m : R →+* S
d : ℕ
U : Set R
h : U.Finite
⊢ Set.Finite fun f ↦ f.natDegree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U

Tactic:
let π : R[X] → Fin (d + 1) → R := fun f i => f.coeff i
      refine ((Set.Finite.pi fun _ => h).subset <| ?_).of_finite_image (?_ : Set.InjOn π _)
      · exact Set.image_subset_iff.2 fun f hf i _ => hf.2 i
      · refine fun x hx y hy hxy => (ext_iff_natDegree_le hx.1 hy.1).2 fun i hi => ?_
        exact id congr_fun hxy ⟨i, Nat.lt_succ_of_le hi⟩

Goal state after:
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]; exact dvd_zero _

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ (Multiset.map (fun a ↦ X - C a) p.roots).prod ∣ p

Tactic:
← map_dvd_map _ (IsFractionRing.injective R <| FractionRing R)
    (monic_multisetProd_X_sub_C p.roots)

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ map (algebraMap R (FractionRing R)) (Multiset.map (fun a ↦ X - C a) p.roots).prod ∣
    map (algebraMap R (FractionRing R)) p
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp : p ≠ 0
s : Multiset R
h : (Multiset.map (fun a ↦ X - C a) s).prod ∣ p
r : R
⊢ (Multiset.map (fun a ↦ X - C a) (Multiset.filter (Eq r) s)).prod ∣ p

Tactic:
exact (Multiset.prod_dvd_prod_of_le <| Multiset.map_le_map <| s.filter_le _).trans h

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

Goal state before:
pp: A : Type u_3
B : Type u_4
inst✝² : Semiring A
inst✝¹ : CommRing B
inst✝ : IsDomain B
f : A →+* B
p : A[X]
hp0 : p ≠ 0
⊢ ↑(map f p).roots.card ≤ p.degree

Tactic:
by
  by_cases hpm0 : p.map f = 0
  · simp [hp0, hpm0, zero_le_degree_iff]
  exact card_roots hpm0 |>.trans degree_map_le

Goal state after:
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
inst✝ : Nontrivial R
x : R
⊢ (aeval ((algebraMap R A) x)) X - (aeval ((algebraMap R A) x)) (C x) = 0

Tactic:
aeval_X,

Goal state after:
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : R
⊢ (algebraMap R A) x - (aeval ((algebraMap R A) x)) (C x) = 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (g a)) (map (↑f) q) = 0
⊢ g ((aeval a) q) = g 0

Tactic:
change aeval ((g : A →+* B) a) _ = 0 at h2

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ g ((aeval a) q) = g 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : -(aeval s) (C (q.coeff 0)) = (aeval s) X * (aeval s) p
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Tactic:
aeval_X,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : -(aeval s) (C (q.coeff 0)) = s * (aeval s) p
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : (aeval s) (q - C (q.coeff 0)) = (aeval s) (X * p)
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)

Tactic:
rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : (aeval s) X ∣ (aeval s) (C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r

Tactic:
aeval_X,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
key : s ∣ (aeval s) (C (q.coeff 0))
⊢ ∃ r, r ≠ 0 ∧ s ∣ (algebraMap R S) r
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
⊢ (aeval x) p.divX * (aeval x) X + (aeval x) (C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)

Tactic:
aeval_X,

Goal state after:
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
⊢ (aeval x) p.divX * x + (aeval x) (C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3
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
aeval_eq : (aeval x) p * (aeval x) X = 0
⊢ (↑x)⁻¹ ∈ A

Tactic:
aeval_X,

Goal state after:
case refine_3
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
aeval_eq : (aeval x) p * x = 0
⊢ (↑x)⁻¹ ∈ A
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
⊢ ∃ C, C.FG ∧ x ∈ Subalgebra.baseChange A C

Tactic:
by
  obtain ⟨S, hS⟩ := TensorProduct.exists_finset x
  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
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
classical
  simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R R _ _),
    ← LinearEquiv.coe_coe, ← coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe,
    EquivLike.injective_comp, lmap_injective]
  constructor <;> (intro h; intros; apply h)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
e : A ≃ₐ[R] B
inst✝ : IsAzumaya R A
x✝² : Module.Projective R B := Module.Projective.of_equiv ↑e
x✝¹ : FaithfulSMul R B := FaithfulSMul.of_injective e (AlgEquiv.injective e)
x✝ : Module.Finite R B := Module.Finite.equiv ↑e
⊢ Function.Bijective (⇑(AlgHom.mulLeftRight R B) ∘ ⇑(Algebra.TensorProduct.congr e (AlgEquiv.op e)))

Tactic:
← AlgEquiv.coe_toAlgHom,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Ring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
e : A ≃ₐ[R] B
inst✝ : IsAzumaya R A
x✝² : Module.Projective R B := Module.Projective.of_equiv ↑e
x✝¹ : FaithfulSMul R B := FaithfulSMul.of_injective e (AlgEquiv.injective e)
x✝ : Module.Finite R B := Module.Finite.equiv ↑e
⊢ Function.Bijective (⇑(AlgHom.mulLeftRight R B) ∘ ⇑↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)))
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 : ι) → InvolutiveStar (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
⊢ ∀ (i : ι) (x : G i), star (star ⟦⟨i, x⟩⟧) = ⟦⟨i, x⟩⟧

Tactic:
intro i x

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✝¹ : (i : ι) → InvolutiveStar (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
i : ι
x : G i
⊢ star (star ⟦⟨i, x⟩⟧) = ⟦⟨i, x⟩⟧
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✝² : Monoid R
inst✝¹ : (i : ι) → MulAction R (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
i : ι
x✝ : G i
⊢ 1 • ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝⟩⟧

Tactic:
by rw [smul_def, one_smul]

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

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

Tactic:
rw [add_comm, dens_sdiff_add_dens_inter]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: R : Type u_1
inst✝ : CommGroup R
f : ℤ → R
N : ℕ
⊢ ∏ m ∈ Icc (-(↑N + 1)) (↑N + 1), f m = f (↑N + 1) * f (-(↑N + 1)) * ∏ m ∈ Icc (-↑N) ↑N, f m

Tactic:
by
  induction N
  · rw [Icc_succ_succ]
    grind
  · rw [Icc_succ_succ, prod_union (by simp)]
    grind

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul.tmul
R✝ : Type u_1
inst✝⁴² : CommSemiring R✝
M₁✝ : Type u_2
M₂✝ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝¹ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝¹ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
y : M₃
x : M₁
z : M₂
⊢ (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (t • hf.equiv (x ⊗ₜ[R] z) ⊗ₜ[S] y) =
    (RingHom.id T) t • (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (hf.equiv (x ⊗ₜ[R] z) ⊗ₜ[S] y)

Tactic:
have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']

Goal state after:
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ x ∈ s with Even (f x), f x + ∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
Nat.even_add

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (Even (∑ x ∈ s with Even (f x), f x) ↔ Even (∑ x ∈ s with ¬Even (f x), f x)) ↔ Even #({x ∈ s | Odd (f x)})
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_2
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
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ f x = 1 • f x

Tactic:
rw [one_smul]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case e'_3
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
Q : Type u_3
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
x : M
hF : ∀ (s : S) (m : M), (h.lift g) (s • f m) = s • g m
⊢ g x = 1 • g x

Tactic:
rw [one_smul]

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

Goal state before:
pp: α : Type u_1
m m' : Multiset α
h : m ≤ m'
⊢ m.sym2 ≤ m'.sym2

Tactic:
induction m, m' using Quotient.inductionOn₂ with | _ xs ys
  suffices xs <+~ ys from this.sym2
  simpa only [quot_mk_to_coe, coe_le, sym2_coe] using h

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2

Tactic:
by
  rw [← image_union, diag_union_offDiag, sym2_eq_image]

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

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ : ℕ
⊢ s.sym (n✝ + 1) = ∅ ↔ n✝ + 1 ≠ 0 ∧ s = ∅

Tactic:
· refine ⟨fun h ↦ ⟨Nat.succ_ne_zero _, eq_empty_of_sym_eq_empty h⟩, ?_⟩
    rintro ⟨_, rfl⟩
    exact sym_empty _

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f'.toFun (s • x) = (RingHom.id S) s • f'.toFun x
hy : f'.toFun (s • y) = (RingHom.id S) s • f'.toFun y
⊢ f'.toFun (s • (x + y)) = (RingHom.id S) s • f'.toFun (x + y)

Tactic:
dsimp at *; rw [smul_add, map_add, map_add, smul_add, hx, hy]

Goal state after: