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

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ (f.prod g).ker = f.ker ⊓ g.ker

Tactic:
by
  rw [ker, ← prod_bot, comap_prod_prod]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_1.add
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
k : ι'
u v : ι ⊕ ι' → R
hx✝ : u ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
hy✝ : v ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)
hu : u (Sum.inr k) = 0
hv : v (Sum.inr k) = 0
⊢ (u + v) (Sum.inr k) = 0

Tactic:
| add u v _ _ hu hv =>

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : Preorder ι
inst✝² : LocallyFiniteOrderBot ι
F : Type u_4
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
f : ι → α
g : F
⊢ ⇑(partialSups (⇑g ∘ f)) = ⇑g ∘ ⇑(partialSups f)

Tactic:
funext _; simp [partialSups]

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
· exact congr_arg _ (funext (not_nonempty_iff.mp hι).elim)

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_min' _ rfl

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 : ι
n : ℕ
h : pred^[n] i0 < i0
⊢ Nat.find ⋯ ≤ n

Tactic:
exact Nat.find_min' _ rfl

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
ih : ∀ (i : ι), #(Iio i) ≤ n → (partialSups (disjointed f)) i = (partialSups f) i
i : ι
hi : #(Iio i) ≤ n + 1
⊢ (partialSups (disjointed f)) i = (partialSups f) i

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
⊢ LeftInverse (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) fun x ↦ ↑x.snd

Tactic:
rintro ⟨n, ⟨k, l⟩, h⟩

Goal state after:
A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
n k l : A
h : (k, l) ∈ mulAntidiagonal n
⊢ (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) ((fun x ↦ ↑x.snd) ⟨n, ⟨(k, l), h⟩⟩) = ⟨n, ⟨(k, l), h⟩⟩
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ toAdd (p.1 * p.2) = toAdd (ofAdd a) ↔ toAdd p.1 + toAdd p.2 = a

Tactic:
toAdd_mul,

Goal state after:
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasAntidiagonal A
a : A
p : Multiplicative A × Multiplicative A
⊢ toAdd p.1 + toAdd p.2 = toAdd (ofAdd a) ↔ toAdd p.1 + toAdd p.2 = a
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonal n = image (fun i ↦ (i, n - i)) (range (n + 1))

Tactic:
simp only [antidiagonal_eq_map, map_eq_image, Function.Embedding.coeFn_mk]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
β : Type v
F : Type w
inst✝ : Semiring α
I : Ideal α
a b a✝ x✝ : α
h : a✝ ∈ ⊥
⊢ a✝ * x✝ ∈ ⊥

Tactic:
by rw [h, zero_mul]; exact zero_mem _

Goal state after:
Module: Mathlib.RingTheory.Ideal.Prime

Goal state before:
pp: case succ
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsPrime
r : α
n : ℕ
ih : r ^ n ∈ I → r ∈ I
H : r ^ (n + 1) ∈ I
⊢ r ∈ I

Tactic:
| succ n ih =>

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
n : ℕ
⊢ t n 0 = y ^ n

Tactic:
simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, Nat.sub_zero]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ a * (1 - a) = 0

Tactic:
rw [mul_sub, mul_one, sub_eq_zero, eq_comm, IsIdempotentElem]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + (a * b + b * a + b) = a + b

Tactic:
hab,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b + b * a = 0
⊢ a + (0 + b) = a + b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b * b - b * a - (a * b - a * a) = b - a

Tactic:
hab,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b * b - b * a - (a - a * a) = b - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * (a * b + b * a) * a = 0

Tactic:
hab,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * 0 * a = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ a * (a * b + b * a) = 0

Tactic:
hab,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
h : a * b * a = 0
⊢ a * 0 = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : b * a = 0
this : a * b = 0
⊢ a * b = b * a

Tactic:
hab,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : b * a = 0
this : a * b = 0
⊢ a * b = 0
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
⊢ (x + y) ^ (n + 1) = ∑ m ∈ range (n + 1 + 1), t (n + 1) m

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y - x * z} = span {x, y}

Tactic:
span_pair_sub_left_mul

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
h : ∃ a, a * (1 - e) = x
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker

Tactic:
obtain ⟨x, rfl⟩ := h

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 - e) ∈ (LinearMap.toSpanSingleton R R e).ker
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = n * (2 * 2 ^ (n - 1))

Tactic:
mul_pow_sub_one h

Goal state after:
n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = n * 2 ^ n
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J

Tactic:
intro J x hIJ hxnI hxJ

Goal state after:
case right
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
⊢ 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ 1 ∈ J

Tactic:
← zero_add (1 : R),

Goal state after:
case right.mk
R : Type u_5
inst✝ : CommRing R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : x ∉ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : (mk I) x * Quot.mk (⇑(Submodule.quotientRel I)) y = 1
⊢ 0 + 1 ∈ J
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (f.iterateMapComap i (n + 1) K) ≤ map i (f.iterateMapComap i (n + 1) K)

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K

Tactic:
| succ n ih =>

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

Goal state before:
pp: case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), ¬⊥ < I ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)

Tactic:
not_bot_lt_iff

Goal state after:
case inr
R : Type u_5
inst✝ : CommSemiring R
h✝ : Nontrivial R
⊢ (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder (Ideal R)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr.mp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ y i = 0 → i ∉ x.support

Tactic:
simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case mpr.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
x : I →₀ N
y : I → M
hy : ∀ (i : I), f (y i) = x i
i : I
⊢ i ∉ x.support → y i = 0

Tactic:
simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

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

Goal state before:
pp: case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
⊢ s ∩ t ⊆ u → p u

Tactic:
hu

Goal state after:
case right
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
⊢ p u
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
⊢ q (s ∩ t)

Tactic:
by
    use inter_mem (mem_iInf_of_mem _ hs) ht.1
    intro u hu
    have : u = (u ∪ s) ∩ (u ∪ t) := by
      rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu
    rw [this]
    exact ins (mem_of_superset hs subset_union_right) (ht.2 _ subset_union_right)

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ t ∈ l ⊓ l' → ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t

Tactic:
simp only [mem_inf_iff, hl.mem_iff, hl'.mem_iff]

Goal state after:
case mp
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ t₁, (∃ i, p i ∧ s i ⊆ t₁) ∧ ∃ t₂, (∃ i, p' i ∧ s' i ⊆ t₂) ∧ t = t₁ ∩ t₂) →
    ∃ i, (p i.fst ∧ p' i.snd) ∧ s i.fst ∩ s' i.snd ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
l : Filter α
⊢ l ≤ comap f ⊤

Tactic:
rw [comap_top]
  exact le_top

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → x ⊆ y → y ∈ ⋃ i, (f i).sets

Tactic:
simp only [mem_iUnion, exists_imp]

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → x ⊆ y → ∃ i, y ∈ (f i).sets
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α}, x ∈ ⋃ i, (f i).sets → y ∈ ⋃ i, (f i).sets → x ∩ y ∈ ⋃ i, (f i).sets

Tactic:
simp only [mem_iUnion, exists_imp]

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
⊢ ∀ {x y : Set α} (x_1 : ι), x ∈ (f x_1).sets → ∀ (x_2 : ι), y ∈ (f x_2).sets → ∃ i, x ∩ y ∈ (f i).sets
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
⊢ WellFoundedGT { N // N.FG }

Tactic:
let f : α ↪o Submodule R M := OrderEmbedding.subtype _

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
f : α ↪o Submodule R M := OrderEmbedding.subtype fun N ↦ N.FG
⊢ WellFoundedGT { N // N.FG }
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_4
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
inst✝³ : CommSemiring R
inst✝² : Algebra R A
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
hS : S.FG
h : Surjective ⇑(algebraMap R A)
⊢ (restrictScalars R S).FG

Tactic:
obtain ⟨s, rfl⟩ := hS
  exact ⟨s, .symm <| restrictScalars_span R A h _⟩

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

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
⊢ Module.Finite A₂ B₂

Tactic:
by
  let := e₁.toRingHom.toAlgebra
  let := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
  have : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
  let e : B₁ ≃ₐ[A₂] B₂ :=
    { e₂ with
      commutes' := fun r ↦ by
        simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r) }
  have := of_restrictScalars_finite A₁ A₂ B₁
  exact equiv e.toLinearEquiv

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case convert_4
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ BddAbove (range Subtype.val)

Tactic:
· use a
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    exact hx.le

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r ((enum r) ⟨(typein r).toRelEmbedding x, ⋯⟩) ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
@enum_lt_enum _ r,

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : a < b
⊢ a - b ≤ c

Tactic:
· simp [sub_eq_zero_of_lt h']

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
h : ∀ (i : o.ToType), o.familyOfBFamily f i ≤ a
i : Ordinal.{u}
hi : i < o
⊢ f i hi ≤ a

Tactic:
rw [← familyOfBFamily_enum o f]
      exact h _

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono (enumOrd s) ∧ range (enumOrd s) = s

Tactic:
exact ⟨enumOrd_strictMono hs, range_enumOrd hs⟩

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
⊢ ⨅ r, type ↑r = ⨅ r, type ↑r

Tactic:
refine congr_arg sInf <| ext fun o ↦ ⟨?_, ?_⟩ <;>
    rintro ⟨⟨r, hr⟩, rfl⟩

Goal state after:
case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r

case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
⊢ o ≤ lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding

Tactic:
by
      by_contra! h
      have h := h.trans_eq (type_toType o).symm
      simpa [typein_enum] using lt_lsub.{u, u} (typein (· < ·)) (enum (· < ·) ⟨_, h⟩)

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
w✝ : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
⊢ ∃ x, ∃ (x_1 : WellFoundedLT α), (#α).ord = typeLT α

Tactic:
exact ⟨this, inferInstance, hr⟩

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c

Tactic:
← card_ord c

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{v}
⊢ Ordinal.lift.{u, v} c.ord = (lift.{u, v} c).ord

Tactic:
refine le_antisymm (le_of_forall_lt fun a ha => ?_) ?_

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

case refine_2
c : Cardinal.{v}
⊢ (lift.{u, v} c).ord ≤ Ordinal.lift.{u, v} c.ord
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b m n : ℕ
h₁ : b ^ m ≤ n
h₂ : n < b ^ (m + 1)
hm : m ≠ 0
⊢ log b n = m

Tactic:
exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b n ≤ log c n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn); · rw [log_zero_right, log_zero_right]
  apply le_log_of_pow_le hc
  calc
    c ^ log b n ≤ b ^ log b n := Nat.pow_le_pow_left hb _
    _ ≤ n := pow_log_le_self _ hn

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun a x ↦ f a) = f o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.blsub fun x x_1 ↦ f x) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a

Goal state after:
case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
o : Ordinal.{u}
ho : IsSuccLimit o
this : (o.bsup fun a x ↦ f a) = f o
⊢ (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
· rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x y : Ordinal.{u_4}
⊢ x * y % x = 0

Tactic:
by
  simpa using mul_add_mod_self x y 0

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ a ^ ω ≤ b

Tactic:
rw [ha, zero_opow omega0_ne_zero]

Goal state after:
case inl
a b : Ordinal.{u_1}
hab : a * b = b
ha : a = 0
⊢ b = 0 ∨ 0 ≤ b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ #Cardinal.{u} = univ.{u, u + 1}

Tactic:
by
  simpa only [card_type, card_univ] using congr_arg card type_lt_cardinal

Goal state after: