mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
hle : ∀ (h : s.Terminates), n ≤ s.length h
⊢ (take n s).length = n

Tactic:
induction n generalizing s with
  | zero => simp [take]
  | succ n ih =>
      rw [take, destruct]
      let ⟨a, ha⟩ := lt_length_iff'.1 (fun ht => lt_of_lt_of_le (Nat.succ_pos _) (hle ht))
      simp only [Option.mem_def.1 ha, Option.map_eq_map, Option.map_some, List.length_cons,
        Nat.add_right_cancel_iff]
      rw [ih]
      intro h
      simp only [length, tail, Nat.le_find_iff, TerminatedAt, get?_mk, Stream'.tail]
      intro m hmn hs
      have := lt_length_iff'.1 (fun ht => (Nat.lt_of_succ_le (hle ht)))
      rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this
      simp at this

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
s : Computation α
f : α → Computation β
a : α
b : β
h1 : s ~> a
h2 : f a ~> b
b' : β
bB : b' ∈ s.bind f
⊢ b = b'

Tactic:
by
  rcases exists_of_mem_bind bB with ⟨a', a's, ba'⟩
  rw [← h1 a's] at ba'; exact h2 ba'

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
⊢ LiftRel R (pure a) (pure b) ↔ R a b

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ s.tail.drop n = s.drop (n + 1)

Tactic:
by
  rw [Nat.add_comm]; symm; apply dropn_add

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case inl
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : some y = (s.set n x).get? n
⊢ p y

Tactic:
by_cases h_term : s.TerminatedAt n
    · simp [get?_set_of_terminatedAt _ h_term] at hy
    · simp_all [get?_set_of_not_terminatedAt _ h_term]

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (2 * (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))

Tactic:
two_mul

Goal state after:
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
R : α → α → Prop
x✝ : α
s✝ : Seq α
h : Pairwise R (cons x✝ s✝)
⊢ Pairwise R (cons x✝ s✝).tail

Tactic:
simp [h.cons_elim.right]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
⊢ g.convs (n + 1) = g.convs' (n + 1)

Tactic:
suffices g.convs (n + 1) = g'.convs' n by
      rwa [succ_nth_conv'_eq_squashGCF_nth_conv']

Goal state after:
case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
n : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) → g.convs n = g.convs' n
g : GenContFract K
s_pos : ∀ {gp : Pair K} {m : ℕ}, m < n + 1 → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF n
⊢ g.convs (n + 1) = g'.convs' n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
⊢ (fun P ↦ ⟨P.toPoly, ⋯⟩) ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }) f) =
    f

Tactic:
by
    ext n
    obtain hn | hn := le_or_gt n 3
    · interval_cases n <;> simp only <;> ring_nf <;> try simp only [coeffs]
    · rw [coeff_eq_zero hn, (degree_le_iff_coeff_zero (f : R[X]) 3).mp f.2]
      simpa using hn

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

Tactic:
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
n_eq_zero : n = 0
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)

case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n ≤ 1 ∨ ¬g.TerminatedAt (n - 2)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
n_eq_zero : n = 0
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - (b⁻¹ * a) • 1).ker = (f - b⁻¹ • a • 1).ker

Tactic:
smul_smul

Goal state after:
K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - (b⁻¹ * a) • 1).ker = (f - (b⁻¹ * a) • 1).ker
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := hN.toFinset
κ : ι → Type u_3 := fun i ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := fun i ↦ Free.chooseBasis R ↥(N ↑i)
h : IsInternal fun i ↦ N ↑i
⊢ ∑ x, 0 = 0

Tactic:
Finset.sum_const_zero

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
⊢ (trace R M) f = 0

Tactic:
have hN : {i | N i ≠ ⊥}.Finite := WellFoundedGT.finite_ne_bot_of_iSupIndep
    h.submodule_iSupIndep
  let s := hN.toFinset
  let κ := fun i ↦ Module.Free.ChooseBasisIndex R (N i)
  let b : (i : s) → Basis (κ i) R (N i) := fun i ↦ Module.Free.chooseBasis R (N i)
  replace h : IsInternal fun i : s ↦ N i := by
    convert! DirectSum.isInternal_ne_bot_iff.mpr h <;> simp [s]
  simp_rw [trace_eq_matrix_trace R (h.collectedBasis b), Matrix.trace,
    diag_toMatrix_directSum_collectedBasis_eq_zero_of_mapsTo_ne h b σ hσ hf (by simp [s]),
    Pi.zero_apply, Finset.sum_const_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
x✝ : ↥p
⊢ ↑((f₂ * f₁) x✝) = ↑((f₁ * f₂) x✝)

Tactic:
simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e r : R
he : IsIdempotentElem e
I : Ideal R
s : R
hs : s ∈ I
t : R
hrst : s - r = e * t
⊢ (1 - e) * r = (1 - e) * s

Tactic:
linear_combination he.eq * t - (1 - e) * hrst

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.fst + x.snd • ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
← inl_mul_eq_smul

Goal state after:
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.fst + inl x.snd * ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case insert
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
⊢ y + z ∈ (f.genEigenspace μ₂) k

Tactic:
let g := f - μ₂ • 1

Goal state after:
case insert
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
⊢ y + z ∈ (f.genEigenspace μ₂) k
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝ : Module.Finite R M
this : Free R M
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
have := Module.Finite.of_basis (b.map e)

Goal state after:
case pos
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝¹ : Module.Finite R M
this✝ : Free R M
this : Module.Finite R N
⊢ (trace R N) (e.conj f) = (trace R M) f
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ (f * (f - (algebraMap K (End K V)) μ) ^ n).range = ((f - (algebraMap K (End K V)) μ) ^ n * f).range

Tactic:
rw [Algebra.mul_sub_algebraMap_pow_commutes]

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.snd
      ({ re := TrivSqZeroExt.fst (x✝ * y✝).re, imI := TrivSqZeroExt.fst (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.fst (x✝ * y✝).imJ, imK := TrivSqZeroExt.fst (x✝ * y✝).imK },
        { re := TrivSqZeroExt.snd (x✝ * y✝).re, imI := TrivSqZeroExt.snd (x✝ * y✝).imI,
          imJ := TrivSqZeroExt.snd (x✝ * y✝).imJ, imK := TrivSqZeroExt.snd (x✝ * y✝).imK }) =
    TrivSqZeroExt.snd
      (({ re := TrivSqZeroExt.fst x✝.re, imI := TrivSqZeroExt.fst x✝.imI, imJ := TrivSqZeroExt.fst x✝.imJ,
            imK := TrivSqZeroExt.fst x✝.imK },
          { re := TrivSqZeroExt.snd x✝.re, imI := TrivSqZeroExt.snd x✝.imI, imJ := TrivSqZeroExt.snd x✝.imJ,
            imK := TrivSqZeroExt.snd x✝.imK }) *
        ({ re := TrivSqZeroExt.fst y✝.re, imI := TrivSqZeroExt.fst y✝.imI, imJ := TrivSqZeroExt.fst y✝.imJ,
            imK := TrivSqZeroExt.fst y✝.imK },
          { re := TrivSqZeroExt.snd y✝.re, imI := TrivSqZeroExt.snd y✝.imI, imJ := TrivSqZeroExt.snd y✝.imJ,
            imK := TrivSqZeroExt.snd y✝.imK }))

Tactic:
dsimp
      congr 1 <;> simp <;> ring

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (b : G₀), 1 • b = b

Tactic:
simp [smul_def]

Goal state after:
Module: Mathlib.Algebra.Field.Action.ConjAct

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
⊢ ∀ (a : ConjAct K), a • 0 = 0

Tactic:
simp [smul_def]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
a : α × Bool
⊢ reduce (a :: reduce L) = reduce (a :: L)

Tactic:
by
  simp

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ Infinite (FreeGroup α)

Tactic:
by
  classical
  exact Infinite.of_surjective FreeGroup.norm FreeGroup.norm_surjective

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type u
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
⊢ #(FreeAlgebra R X) = max (max #R #X) ℵ₀

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type u
inst✝ : IsEmpty X
⊢ #(FreeAlgebra R X) = #R

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ ↑↑(Int.negSucc n) = -↑(n + 1)

Tactic:
by
    change coe _ = -coe _
    rw [Int.cast_negSucc, coe_neg]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
⊢ IsIntegrallyClosed R

Tactic:
rw [isIntegrallyClosed_iff (K := FractionRing R)]

Goal state after:
R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
this : IsDomain R
f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom ⋯
⊢ ∀ {x : FractionRing R}, IsIntegral R x → ∃ y, (algebraMap R (FractionRing R)) y = x
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ • x✝

Tactic:
ext <;> exact NNRat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y

Tactic:
rw [mul_assoc, Module.End.mul_apply, this, Module.End.intCast_apply, map_smul,
      Pi.smul_apply, shiftₗ_pow_apply]

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] (P.leadingCoeff • ↑P.natDegree !)) x = 0 x

Tactic:
Pi.smul_def

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] fun i ↦ P.leadingCoeff • ↑P.natDegree ! i) x = 0 x
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ Nat.card ↑(a • s) = Nat.card ↑s

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (fun a ↦ ∑ x ∈ range n, (P x • Δ_[1]^[n] fun i ↦ i ^ x) a) = 0

Tactic:
← sum_fn

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
P : ℕ → R
⊢ (∑ c ∈ range n, P c • Δ_[1]^[n] fun i ↦ i ^ c) = 0
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ (Units.mk0 (f r₁) hr₁)⁻¹ * (Units.mk0 (f r₂) hr₂)⁻¹ * (Units.mk0 (f s₁) hs₁ * Units.mk0 (f s₂) hs₂) =
    (Units.mk0 (f r₁) ⋯ * Units.mk0 (f r₂) ⋯)⁻¹ * (Units.mk0 (f s₁) ⋯ * Units.mk0 (f s₂) ⋯)

Tactic:
mul_inv

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ (Units.mk0 (f r₁) hr₁)⁻¹ * (Units.mk0 (f r₂) hr₂)⁻¹ * (Units.mk0 (f s₁) hs₁ * Units.mk0 (f s₂) hs₂) =
    (Units.mk0 (f r₁) ⋯)⁻¹ * (Units.mk0 (f r₂) ⋯)⁻¹ * (Units.mk0 (f s₁) ⋯ * Units.mk0 (f s₂) ⋯)
Module: Mathlib.Order.Category.LinOrd

Goal state before:
pp: X Y : LinOrd
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Category.LinOrd

Goal state before:
pp: X Y : LinOrd
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ { down := 0 } ≤ { down := 0 }

Tactic:
apply Fin.zero_le

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 0 } ≤ { down := 1 }

Tactic:
apply Fin.zero_le

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

Tactic:
apply Fin.zero_le

Goal state after:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }

Tactic:
apply Fin.zero_le

Goal state after:
case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 0 } ≤ { down := 0 }

Tactic:
apply Fin.zero_le

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 0 } ≤ { down := 1 }

Tactic:
apply Fin.zero_le

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

Tactic:
apply Fin.zero_le

Goal state after:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }