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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
hv : LinearIndependent R v
inst✝ : Nontrivial R
x : ↥(span R (range v))
⊢ Span.repr R (range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)

Tactic:
have p :
    (Span.repr R (Set.range v) x).equivMapDomain (Equiv.ofInjective _ hv.injective).symm =
      hv.repr x := by
    apply (LinearIndependent.linearCombinationEquiv hv).injective
    ext
    simp only [LinearIndependent.linearCombinationEquiv_apply_coe, Equiv.self_comp_ofInjective_symm,
      LinearIndependent.linearCombination_repr, Finsupp.linearCombination_equivMapDomain,
      Span.finsupp_linearCombination_repr]
  ext ⟨_, ⟨i, rfl⟩⟩
  simp [← p]

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

Goal state before:
pp: case right
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]

Tactic:
· exact h

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

Goal state before:
pp: a b c : ℕ
hc : c ≤ a % c + b % c
hc0 : 0 < c
⊢ (a + b) / c = a / c + b / c + 1

Tactic:
by rw [Nat.add_div hc0, if_pos hc]

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

Goal state before:
pp: α : Type u_3
⊢ card α ≠ 0 ↔ Nonempty α

Tactic:
by
  simp [card_eq_zero_iff_empty]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ Module.rank R M = 1

Tactic:
rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]

Goal state after:
case h₁
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ 1

case h₂
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton R
⊢ ∀ w < 1, ∃ i, w < #↑↑i
Module: Mathlib.LinearAlgebra.Basis.Submodule

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
⊢ (N' : Submodule R M) → N' ≤ ⊥ → (x : M) → x ∈ ⊥ → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N'

Tactic:
intro N _ x x_mem x_ortho

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝³ : Ring R
inst✝² : IsDomain R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
b✝ : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N✝ : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N✝), LinearIndependent R (Subtype.val ∘ v) → m ≤ n
this : DecidableEq M
N : Submodule R M
a✝ : N ≤ ⊥
x : M
x_mem : x ∈ ⊥
x_ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0
⊢ P N
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t

Tactic:
rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
⊢ 1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
one_lt_ncard hs

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Module: Mathlib.GroupTheory.Congruence.Basic

Goal state before:
pp: case mul
M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M ≃* N
rel : N → N → Prop
n1 n2 w x y z : N
a✝¹ : ConGen.Rel rel w x
a✝ : ConGen.Rel rel y z
ih : ∀ ⦃a b : M⦄, f a = w → f b = x → (conGen fun x y ↦ rel (f x) (f y)) a b
ih1 : ∀ ⦃a b : M⦄, f a = y → f b = z → (conGen fun x y ↦ rel (f x) (f y)) a b
a b : M
fa : a = f.symm w * f.symm y
fb : b = f.symm x * f.symm z
⊢ (conGen fun x y ↦ rel (f x) (f y)) (f.symm w * f.symm y) (f.symm x * f.symm z)

Tactic:
exact ConGen.Rel.mul (ih (by simp) (by simp)) (ih1 (by simp) (by simp))

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

Goal state before:
pp: case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ Nontrivial (RingCon R) ↔ Nontrivial R

Tactic:
simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]

Goal state after:
case inl
R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
h✝ : Subsingleton R
⊢ Subsingleton (RingCon R) ↔ Subsingleton R
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
M : Type v
ι : Type x
inst✝⁷ : Semiring R
S : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : SMulCommClass R S M
f : ι → M
g : ι → R
⊢ ((piRing R M ι S).symm f) g = ∑ i, g i • f i

Tactic:
by
  simp [piRing, LinearMap.lsum_apply]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : PredOrder α
a b : α
h : a < b
⊢ ↑(insert (pred b) (Ico a (pred b))) = ↑(Ico a b)

Tactic:
by simpa using Set.insert_Ico_pred_right_eq_Ico h

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ (snd R M M₂).range = ⊤

Tactic:
rw [range_eq_map, ← prod_top, prod_map_snd]

Goal state after:
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s.toFinset, a ⊓ id a_1

Tactic:
Set.mem_toFinset

Goal state after:
case e'_4
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b = ⨆ a_1 ∈ s, a ⊓ id a_1
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s.toFinset, a ⊔ id a_1

Tactic:
Set.mem_toFinset

Goal state after:
case e'_3
ι : Type u_1
α : Type u_2
inst✝³ : Fintype ι
inst✝² : Fintype α
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a : α
s : Set α
⊢ ⨅ b ∈ s, a ⊔ b = ⨅ a_1 ∈ s, a ⊔ id a_1
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f d : ι → α
hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)
hsups : partialSups d = partialSups f
⊢ d = disjointed d

Tactic:
exact funext fun _ ↦ (disjointed_eq_self (fun _ hj ↦ hdisj hj)).symm

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

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

Tactic:
h.eq,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a - (a - a) = 1 - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a - a * a = 0

Tactic:
h.eq,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ a - a = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ a * b + a * b - b * (a * b) = a * b

Tactic:
h.eq,

Goal state after:
R : Type u_1
inst✝ : NonUnitalRing R
a b : R
h : Commute a b
ha : IsIdempotentElem a
hb : IsIdempotentElem b
⊢ b * a + b * a - b * (b * a) = b * a
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = 0

Tactic:
by
  classical
  rw [sum_powerset_neg_one_pow_card]
  exact if_neg (nonempty_iff_ne_empty.mp h0)

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

Goal state before:
pp: α : Type u
β : Type v
f : β → Filter α
s : Set β
h : DirectedOn (f ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) s
ne : s.Nonempty
t : Set α
⊢ t ∈ ⨅ i ∈ s, f i ↔ ∃ i ∈ s, t ∈ f i

Tactic:
have := ne.to_subtype
  simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
π : α → Type u_6
π' : β → Type u_7
f : α → β
hf : Function.Injective f
g : (a : α) → π a → π' (f a)
a : α
l : Filter (π' (f a))
⊢ map (Sigma.mk a) (comap (g a) l) = comap (Sigma.map f g) (map (Sigma.mk (f a)) l)

Tactic:
refine (((basis_sets _).comap _).map _).eq_of_same_basis ?_
  convert! ((basis_sets l).map (Sigma.mk (f a))).comap (Sigma.map f g)
  apply image_sigmaMk_preimage_sigmaMap hf

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht : t ∈ g.seq x
⊢ s.seq t ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq t ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (α → α × β)
hs✝ : s ∈ map (fun b a ↦ (a, b)) g
t : Set α
ht : t ∈ f
u : Set β
hu : u ∈ g
hs : (fun b a ↦ (a, b)) '' u ⊆ s
⊢ (Prod.mk '' t).seq u ∈ (map Prod.mk f).seq g

Tactic:
exact seq_mem_seq (image_mem_map ht) hu

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
s : Set (β → α × β)
hs✝ : s ∈ map Prod.mk f
t : Set β
ht : t ∈ g
u : Set α
hu : u ∈ f
hs : Prod.mk '' u ⊆ s
⊢ ((fun b a ↦ (a, b)) '' t).seq u ∈ (map (fun b a ↦ (a, b)) g).seq f

Tactic:
exact seq_mem_seq (image_mem_map ht) hu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → Filter β
⊢ (map f (𝓟 s)).join = ⨆ x ∈ s, f x

Tactic:
simp only [sSup_image, join_principal_eq_sSup, map_principal]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
p : P
x✝ : p ∈ ⊤
⊢ p ∈ ⇑f '' ↑(span R s)

Tactic:
by simpa [hs] using hf p

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
d : Set α
hD : d ∈ D
hdu✝ : d ⊆ s ∪ t
hdu : d ⊆ t ∪ s
hd₀ : d.Nonempty
hd₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
hdst✝ : d ∩ s ∪ d ∩ t = d
hdst : d ∩ t ∪ d ∩ s = d
this :
  ∀ {α : Type u_1} {s t : Set α} {D : Set (Set α)} [inst : Preorder α],
    IsLowerSet D →
      DirSupClosedOn D s →
        DirSupClosedOn D t →
          ∀ ⦃d : Set α⦄,
            d ∈ D →
              d ⊆ s ∪ t →
                d.Nonempty →
                  DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d →
                    ∀ ⦃a : α⦄,
                      IsLUB d a →
                        d ∩ s ∪ d ∩ t = d →
                          DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) → a ∈ s ∪ t
h : ¬(DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s))
⊢ DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (d ∩ t ∪ d ∩ s)

Tactic:
by rwa [hdst]

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

Goal state before:
pp: R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
⊢ ∀ (a₁ : Submodule R V), Module.Finite R ↥a₁ → ∀ (a₂ : Submodule R V), Module.Finite R ↥a₂ → Module.Finite R ↥(a₁ ⊔ a₂)

Tactic:
intro S₁ hS₁ S₂ hS₂

Goal state after:
R : Type u_2
V : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst✝ : ∀ (i : ι), Module.Finite R ↥(S i)
S₁ : Submodule R V
hS₁ : Module.Finite R ↥S₁
S₂ : Submodule R V
hS₂ : Module.Finite R ↥S₂
⊢ Module.Finite R ↥(S₁ ⊔ S₂)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case inr
R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : x ≤ 0
⊢ x ∈ Submodule.span R≥0 {1, -1}

Tactic:
· simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨-x, neg_nonneg.mpr hx⟩ (x := -1)
      (Submodule.subset_span <| by simp)

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
⊢ ↑((enum s hs) (succ a)) ≤ o

Tactic:
refine enum_le_of_forall_lt ha fun b hb ↦ H.trans_le' ?_

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
b : α
hb : b < succ a
⊢ ↑((enum s hs) b) ≤ ↑((enum s hs) a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
a c : Ordinal.{u_4}
⊢ a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d

case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
rw [mul_add_one, lt_add_iff hb]

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

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
⊢ log b n < c + 1 ↔ log b (n / b) + 1 < c + 1

Tactic:
· have : n / b ≠ 0 := by simp [*, Nat.ne_zero_of_lt h]
    rw [log_lt_iff_lt_pow, Nat.add_lt_add_iff_right, log_lt_iff_lt_pow,
      Nat.pow_add_one, Nat.div_lt_iff_lt_mul] <;> grind

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

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

Tactic:
rw [Nat.pow_one] at h₂
    exact log_of_lt h₂

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

Goal state before:
pp: a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
a : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit 0

case inr
a b : Ordinal.{u_4}
h : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * (y / z) = x * (y % z) + w

Tactic:
apply sub_eq_of_add_eq

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
⊢ log b 0 = 0

Tactic:
obtain rfl | hb := eq_or_ne b 0

Goal state after:
case inl
⊢ log 0 0 = 0

case inr
b : Ordinal.{u_1}
hb : b ≠ 0
⊢ log b 0 = 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ ¬BddAbove (⋂ i, fixedPoints (f i))

Tactic:
rw [not_bddAbove_iff]
  refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩
  rintro _ ⟨i, rfl⟩
  exact nfpFamily_fp (H i) _

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o + o % 2 ^ log 2 o = o

Tactic:
convert! div_add_mod .. using 2
  rw [div_two_opow_log ho, mul_one]

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

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * (↑n + 1) ≤ a

pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ a % ω ^ log ω a < ω ^ log ω a

Tactic:
· rw [Ordinal.mul_le_iff_le_div, hn] <;> simp

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ a % ω ^ log ω a < ω ^ log ω a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a

Tactic:
by simpa only [nfp_fp H] using H.monotone h

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

Goal state before:
pp: ⊢ typeLT Cardinal.{u_1} ≤ (cof Cardinal.{u_1}).ord

Tactic:
by simp [Order.cof_cardinal]

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

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ max (ℵ_ o₁) (ℵ_ o₂) = ℵ_ (max o₁ o₂)

Tactic:
aleph_max

Goal state after:
o₁ o₂ : Ordinal.{u_1}
⊢ max (ℵ_ o₁) (ℵ_ o₂) = max (ℵ_ o₁) (ℵ_ o₂)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c

Tactic:
rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)

Goal state after:
case inl
a b : Ordinal.{u}
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0

case inr.inl
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c

case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
⊢ a * b < ω ^ c
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
this : span R (⇑↑b.repr '' s) = ⊤
⊢ Finite ι

Tactic:
exact finite_of_span_finite_eq_top_finsupp (hs.image _) this

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
⊢ filter p (single i x) = if p i then single i x else 0

Tactic:
ext j
  have := apply_ite (fun x : Π₀ i, β i => x j) (p i) (single i x) 0
  dsimp at this
  grind

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
⊢ ∀ (a b : { l // ∀ (i : ι), i ∈ l }),
    a ≈ b →
      Quotient.map (fun a_2 i ↦ a_2 i ⋯) ⋯ (listChoice fun i x ↦ q i) =
        Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i)

Tactic:
intro _

Goal state after:
case refine_2
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
β : Sort u_3
q : (i : ι) → Quotient (S i)
e : Quotient (Subtype.instSetoid_mathlib fun l ↦ ∀ (i : ι), i ∈ l) :=
  (Equiv.subtypeQuotientEquivQuotientSubtype (fun l ↦ ∀ (i : ι), i ∈ l) (fun s ↦ ∀ (i : ι), i ∈ s) ⋯ ⋯)
    ⟨Finset.univ.val, ⋯⟩
a✝ : { l // ∀ (i : ι), i ∈ l }
⊢ ∀ (b : { l // ∀ (i : ι), i ∈ l }),
    a✝ ≈ b →
      Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i) =
        Quotient.map (fun a i ↦ a i ⋯) ⋯ (listChoice fun i x ↦ q i)
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
⊢ (⟨i, a⟩ ∈ (↑s).toFinset.attach.val.bind fun i ↦ Multiset.map (Sigma.mk ↑i) ↑(fs i)) ∨ (f ⟨i, a⟩.fst) ⟨i, a⟩.snd = 0

Tactic:
cases (fs ⟨i, Multiset.mem_toFinset.mpr hi⟩).prop a with
            | inl ha =>
              left; rw [Multiset.mem_bind]
              use ⟨i, Multiset.mem_toFinset.mpr hi⟩
              constructor
              case right => simp [ha]
              case left => apply Multiset.mem_attach
            | inr ha => right; simp [toFun_eq_coe (f i) ▸ ha]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : ι → Submodule R N
x : N
⊢ x ∈ iSup p ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Tactic:
rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]

Goal state after:
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case mpr.refine_1
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, ↑(μ i) = a
i : ι
hi : i ∈ ↑s
⊢ ↑⟨i, hi⟩ ∈ s

Tactic:
· exact hi

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R✝ : Type u_1
R₂✝ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴⁶ : Semiring R✝
inst✝⁴⁵ : Semiring R₂✝
inst✝⁴⁴ : Semiring S
inst✝⁴³ : Semiring S₂
M✝ : Type u_5
M₂ : Type u_6
N✝ : Type u_7
N₂ : Type u_8
P✝ : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝⁴² : AddCommMonoid M✝
inst✝⁴¹ : AddCommMonoid M₂
inst✝⁴⁰ : AddCommMonoid N✝
inst✝³⁹ : AddCommMonoid N₂
inst✝³⁸ : AddCommMonoid P✝
inst✝³⁷ : AddCommMonoid P₂
inst✝³⁶ : AddCommMonoid Pₗ
inst✝³⁵ : Module R✝ M✝
inst✝³⁴ : Module R✝ M₂
inst✝³³ : Module S N✝
inst✝³² : Module S N₂
inst✝³¹ : Module R₂✝ P✝
inst✝³⁰ : Module S₂ P✝
inst✝²⁹ : Module R✝ P₂
inst✝²⁸ : Module S₂ P₂
inst✝²⁷ : Module R✝ Pₗ
inst✝²⁶ : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²⁵ : AddCommGroup M'
inst✝²⁴ : AddCommGroup P'
inst✝²³ : Module R✝ M'
inst✝²² : Module R₂✝ P'
inst✝²¹ : Module S₂ P'
inst✝²⁰ : SMulCommClass S₂ R₂✝ P✝
inst✝¹⁹ : SMulCommClass S R✝ Pₗ
inst✝¹⁸ : SMulCommClass S₂ R₂✝ P'
inst✝¹⁷ : SMulCommClass S₂ R✝ P₂
ρ₁₂ : R✝ →+* R₂✝
σ₁₂✝ : S →+* S₂
R : Type u_14
R₂ : Type u_15
R₃ : Type u_16
R₄ : Type u_17
R₅ : Type u_18
M : Type u_19
N : Type u_20
P : Type u_21
Q : Type u_22
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
inst✝¹³ : Semiring R₄
inst✝¹² : Semiring R₅
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : AddCommMonoid P
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R M
inst✝⁶ : Module R₂ N
inst✝⁵ : Module R₃ P
inst✝⁴ : Module R₄ Q
inst✝³ : Module R₅ P
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
inst✝ : SMulCommClass R₃ R₅ P
σ₁₅ : R →+* R₅
h : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P
g : Q →ₛₗ[σ₄₂] N
x✝¹ x✝ : M
⊢ (lcompₛₗ R₅ P σ₂₃ g) (h (x✝¹ + x✝)) = (lcompₛₗ R₅ P σ₂₃ g) (h x✝¹) + (lcompₛₗ R₅ P σ₂₃ g) (h x✝)

Tactic:
simp [map_add]

Goal state after: