mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ (truncate n).comp (lift f f_compat) = f n

Tactic:
ext1

Goal state after:
p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
x✝ : S
⊢ ((truncate n).comp (lift f f_compat)) x✝ = (f n) x✝
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ verschiebung (x.shift 1) = verschiebung (frobenius ((frobeniusEquiv p k).symm (x.shift 1)))

Tactic:
← frobeniusEquiv_apply,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ verschiebung (x.shift 1) = verschiebung ((frobeniusEquiv p k) ((frobeniusEquiv p k).symm (x.shift 1)))
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = (aeval x) 1 * Real.exp (-(x ^ 2 / 2))

Tactic:
map_one,

Goal state after:
case zero
x : ℝ
⊢ Real.exp (-(x ^ 2 / 2)) = 1 * Real.exp (-(x ^ 2 / 2))
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
⊢ deriv^[n + 1] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))

Tactic:
have deriv_gaussian :
      deriv (fun y => Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2)) := by
      -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [mul_comm, ← neg_mul]`
      rw [deriv_exp (by simp)]
      simp [mul_comm]

Goal state after:
case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ deriv^[n + 1] (fun y ↦ Real.exp (-(y ^ 2 / 2))) x =
    (-1) ^ (n + 1) * ((aeval x) (hermite (n + 1)) * Real.exp (-(x ^ 2 / 2)))
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ y * y + y⁻¹ * y - x * y = 0 ↔ y ^ 2 - x * y + 1 = 0

Tactic:
inv_mul_cancel₀ hy

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
x✝ : x ∈ {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}
φ : K[X] := X ^ 2 - C x * X + 1
hφ : φ ≠ 0
y : K
hy : ¬y = 0
⊢ y * y + 1 - x * y = 0 ↔ y ^ 2 - x * y + 1 = 0
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (X ^ n - X - 1)

Tactic:
rw [hn0, pow_zero, sub_sub, add_comm, ← sub_sub, sub_self, zero_sub]

Goal state after:
case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: case pos
n : ℕ
hn1 : n ≠ 1
hn0 : n = 0
⊢ Irreducible (-X)

Tactic:
exact Associated.irreducible ⟨-1, mul_neg_one X⟩ irreducible_X

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

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ False

Tactic:
apply X_pow_sub_X_sub_one_irreducible_aux (n := n) z

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
z : ℂ
h1 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1) = 0
h2 : (aeval z) (trinomial 0 1 n ↑(-1) ↑(-1) ↑1).mirror = 0
⊢ z ^ n = z + 1 ∧ z ^ n + z ^ 2 = 0
Module: Mathlib.RingTheory.PowerSeries.CoeffMulMem

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I J : Ideal A
f g : A⟦X⟧
n : ℕ
hf : ∀ i ≤ n, (coeff i) f ∈ I
hg : ∀ i ≤ n, (coeff i) g ∈ J
i : ℕ
hi : i ≤ n
⊢ ∑ p ∈ Finset.antidiagonal i, (coeff p.1) f * (coeff p.2) g ∈ I * J

Tactic:
exact Ideal.sum_mem _ fun p hp ↦ Ideal.mul_mem_mul
    (hf _ ((Finset.HasAntidiagonal.antidiagonal.fst_le hp).trans hi))
    (hg _ ((Finset.HasAntidiagonal.antidiagonal.snd_le hp).trans hi))

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| r • (MvPowerSeries.expand p hp) 1

Tactic:
map_one,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| r • 1
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ (coeff m) ((expand p hp) φ) = 0

Tactic:
by
  rw [coeff, expand, MvPowerSeries.coeff_expand_of_not_dvd (i := ())]
  simpa

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
this :
  ∑ x ∈ range n, (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder =
    ∑ x ∈ range n, if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0
x : ℕ
hx : x ∈ Ico 1 n
hx' : 0 < x
⊢ (if 0 < x then (x - 1).largeSchroder * (n - x).largeSchroder else 0) = (x - 1).largeSchroder * (n - x).largeSchroder

Tactic:
rw [if_pos hx']

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ MvPowerSeries.constantCoeff f - MvPowerSeries.constantCoeff 1 = 0

Tactic:
map_one,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
f : A⟦X⟧
hf : constantCoeff f = 1
⊢ MvPowerSeries.constantCoeff f - 1 = 0
Module: Mathlib.RingTheory.Regular.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
inst✝ : FaithfullyFlat R S
f : M →ₗ[R] N
hf : IsBaseChange S f
rs : List R
reg : IsRegular M rs
⊢ IsRegular N (List.map (⇑(algebraMap R S)) rs)

Tactic:
by
  refine ⟨reg.1.of_flat_of_isBaseChange hf, ?_⟩
  rw [← Ideal.map_ofList]
  exact ((hf.map_smul_top_ne_top_iff_of_faithfullyFlat R M _).mpr reg.2.symm).symm

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

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ toFun S (g.comp f) m = toFun S g (toFun S f m)

Tactic:
simp only [toFun_comp, Function.comp_apply]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic R ↥N ↔ ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥a], IsIsotypicOfType R ↥N ↥a

Tactic:
IsIsotypic

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
⊢ ∃ n, ∃ (_ : NeZero n), ∃ S, IsSimpleModule R ↥S ∧ Nonempty (M ≃ₗ[R] Fin n → ↥S)

Tactic:
by
  have ⟨S, hS⟩ := IsAtomic.exists_atom (Submodule R M)
  rw [← isSimpleModule_iff_isAtom] at hS
  have ⟨n, e⟩ := (h S).linearEquiv_fun
  exact ⟨n, neZero_iff.2 <| by rintro rfl; exact not_subsingleton _ (e.some.subsingleton), S, hS, e⟩

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w✝¹ : (i : Fin n) → DivisionRing (D i)
w✝ : (i : Fin n) → Algebra R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
this : Module.Finite R₀ ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
i : Fin n
⊢ Module.Finite R₀ (D i)

Tactic:
let l := Matrix.entryLinearMap R₀ (D i) 0 0 ∘ₗ
    .proj (φ := fun i ↦ Matrix (Fin (d i)) (Fin (d i)) _) i

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w✝¹ : (i : Fin n) → DivisionRing (D i)
w✝ : (i : Fin n) → Algebra R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
this : Module.Finite R₀ ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
i : Fin n
l : ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)) →ₗ[R₀] D i :=
  Matrix.entryLinearMap R₀ (D i) 0 0 ∘ₗ LinearMap.proj i
⊢ Module.Finite R₀ (D i)
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact

Goal state before:
pp: case refine_1
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ ↑R f' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)) =
    TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) ∘ₗ
      ↑R (LinearMap.baseChange S f)

Tactic:
ext s m

Goal state after:
case refine_1
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
s : S
m : M₁
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑R f' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁))))
        s)
      m =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) ∘ₗ
            ↑R (LinearMap.baseChange S f)))
        s)
      m
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact

Goal state before:
pp: case refine_2
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ ↑R g' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) =
    TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)) ∘ₗ
      ↑R (LinearMap.baseChange S g)

Tactic:
ext s m

Goal state after:
case refine_2
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
s : S
m : M₂
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑R g' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂))))
        s)
      m =
    ((TensorProduct.AlgebraTensorModule.curry
          (TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)) ∘ₗ
            ↑R (LinearMap.baseChange S g)))
        s)
      m
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
⊢ IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (𝕎 k)

Tactic:
by
    refine ⟨p, irreducible p, fun {x} hx => ?_⟩
    obtain ⟨n, b, hb⟩ := exists_eq_pow_p_mul' x hx
    exact ⟨n, b, hb.symm⟩

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
            (↑p ^ (n + 1) * X (1, n + 1)) +
          ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)))) =
    remainder p n +
      (-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        (↑p ^ (n + 1) * X (0, n + 1) *
            ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
          (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
            (↑p ^ (n + 1) * X (1, n + 1) *
                ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
              ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1))))))

Tactic:
apply congrArg (Add.add _)

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
⊢ ↑p ^ (n + 1) * X (0, n + 1) *
        ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
      ((∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))) *
          (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1))) =
    -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
      (↑p ^ (n + 1) * X (0, n + 1) *
          ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
        (↑p ^ (n + 1) * X (0, n + 1) * (↑p ^ (n + 1) * X (1, n + 1)) +
          (↑p ^ (n + 1) * X (1, n + 1) *
              ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1) * (↑p ^ (n + 1) * X (0, n + 1)))))
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)

Tactic:
simp only [polyOfInterest, mul_sub, mul_add, sub_eq_iff_eq_add']
  rw [mul_polyOfInterest_aux4 p n]
  ring

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := ⋯
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ IsLUB (range fun n ↦ f ⟨t, ht⟩ (g n)) (sSup (range g))

Tactic:
refine ⟨?_, fun b hb ↦ csSup_le' ?_⟩ <;> rintro _ ⟨n, rfl⟩
    · apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
      · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)
      · use ⟨t, ht⟩
    · exact (hf ⟨t, ht⟩ _).2.trans <| hb ⟨_, rfl⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k // k < n ∧ p k } ≤ Cardinal.mk ↑{k | p k}

Tactic:
exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
⊢ y ∈ pullSub T x → ∃ z ∈ T, y = x ++ z

Tactic:
intro ⟨h1, h2⟩; use y.drop x.length, h2
    nth_rw 1 [← List.take_append_drop x.length y]
    simpa [-List.take_append_drop, List.prefix_iff_eq_take, hl] using h1

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)

Tactic:
intro ⟨h, _⟩

Goal state after:
case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right✝ : List.drop x.length z ∈ pullSub T y
⊢ z ∈ pullSub T (x ++ y)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case neg.mpr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub T (x ++ y) → z ∈ pullSub (pullSub T y) x

Tactic:
intro ⟨h, _⟩

Goal state after:
case neg.mpr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take (x ++ y).length z <+: x ++ y
right✝ : List.drop (x ++ y).length z ∈ T
⊢ z ∈ pullSub (pullSub T y) x
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ Decidable (a ∈ b.cons' l₂)

Tactic:
haveI :=
        have : sizeOf (⟨_, b⟩ : Lists α) < 1 + 1 + sizeOf b + sizeOf l₂ := by simp [sizeof_pos]
        Equiv.decidable a ⟨_, b⟩
      haveI :=
        have :
          SizeOf.sizeOf a + SizeOf.sizeOf l₂ <
            SizeOf.sizeOf a + SizeOf.sizeOf (Lists'.cons' b l₂) := by
          decreasing_tactic
        mem.decidable a l₂
      refine decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) ?_
      rw [← Lists'.mem_cons]; rfl

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
hb : (PSet.mk γ Γ).Equiv (B b)
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)

Tactic:
eb

Goal state after:
case mk.mk
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
hb : (PSet.mk γ Γ).Equiv (PSet.mk δ Δ)
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ (x ∪ y).rank ≤ max x.rank y.rank

pp: case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank

Tactic:
· simp_rw [rank_le_iff, mem_union, lt_max_iff]
    intro
    apply Or.imp <;> apply rank_lt_of_mem

Goal state after:
case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ o < Γ_ 0 ↔ ∃ n, o < (fun a ↦ veblen a 0)^[n] 0

Tactic:
rw [gamma_zero_eq_nfp, lt_nfp_iff]

Goal state after:
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x y z : Class.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
⊢ y ∈ z

Tactic:
by
  obtain ⟨w, rfl, hw⟩ := hy
  exact coe_mem.2 (hw z hz)

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: d : ℕ
R : Type u_3
A : Type u_4
inst✝³ : Semifield R
inst✝² : Semifield A
inst✝¹ : Algebra R A
a : A
inst✝ : d.AtLeastTwo
⊢ (1 / OfNat.ofNat d) • a = 1 / OfNat.ofNat d * a

Tactic:
simp [Algebra.smul_def, ← nat_rawCast_2]

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n d : ℕ
R : Type u_3
A : Type u_4
inst✝⁴ : Semifield R
inst✝³ : Semifield A
inst✝² : Algebra R A
a : A
inst✝¹ : n.AtLeastTwo
inst✝ : d.AtLeastTwo
⊢ (OfNat.ofNat n / OfNat.ofNat d) • a = OfNat.ofNat n / OfNat.ofNat d * a

Tactic:
simp [Algebra.smul_def, ← nat_rawCast_2]

Goal state after: