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

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₂
f : M →ₗ[R] M₂
I : Type u_1
x✝ : I → M₂
hx : x✝ ∈ Submodule.pi Set.univ fun x ↦ f.range
⊢ x✝ ∈ (f.compLeft I).range

Tactic:
choose y hy using hx

Goal state after:
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₂
f : M →ₗ[R] M₂
I : Type u_1
x✝ : I → M₂
y : (i : I) → i ∈ Set.univ → M
hy : ∀ (i : I) (a : i ∈ Set.univ), f (y i a) = x✝ i
⊢ x✝ ∈ (f.compLeft I).range
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: case refine_2
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
⊢ x ∈ span R (Set.range fun i ↦ single (Sum.inl i) 1)

Tactic:
suffices x = ∑ i : ι, x (Sum.inl i) • Pi.single (M := fun _ ↦ R) (Sum.inl i) (1 : R) by
      rw [this]
      exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i

Goal state after:
case refine_2
R : Type u
ι : Type x
ι' : Type x'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Finite ι
inst✝ : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
⊢ x = ∑ i, x (Sum.inl i) • single (Sum.inl i) 1
Module: Mathlib.Algebra.Order.Interval.Finset.SuccPred

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrder α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (b - 1)) = Ioc a b

Tactic:
by
  simpa [pred_eq_sub_one] using insert_Ioc_pred_right_eq_Ioc h

Goal state after:
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
η : Type u_1
inst✝ : Semiring R
s : ι → η
r : R
f : ι → R
⊢ extend s (r • f) 0 = (RingHom.id R) r • extend s f 0

Tactic:
by simpa using Function.extend_smul r s f 0

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: case mp.left
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.fst R M M₂) q ≤ p₁

pp: case mp.right
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂

Tactic:
· rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1

Goal state after:
case mp.right
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₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
h : q ≤ p₁.prod p₂
⊢ map (LinearMap.snd R M M₂) q ≤ p₂
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₁ (e₂ i) = i

Tactic:
he₁₂

Goal state after:
R : Type u_3
S : Type u_4
G : Type u_5
H : Type u_6
I : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
inst✝⁶ : RingHomSurjective σ
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : AddCommMonoid H
inst✝² : Module S H
inst✝¹ : AddCommMonoid I
inst✝ : Module S I
f : G →ₛₗ[σ] H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf₂ : Surjective (Prod.snd ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : H →ₗ[S] I
he₁ : f.range = e₁.graph
e₂ : I →ₗ[S] H
he₂ : (↑(LinearEquiv.prodComm S H I) ∘ₛₗ f).range = e₂.graph
he₁₂ : ∀ (h : H) (i : I), e₁ h = i ↔ e₂ i = h
i : I
⊢ e₂ i = e₂ i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
i : ι
hi : i < hι.some
⊢ (fun n ↦ if 0 ≤ n then succ^[n.toNat] hι.some else pred^[(-n).toNat] hι.some) (toZ hι.some i) = i

Tactic:
have h_neg : toZ hι.some i < 0 := toZ_neg hi
      simp_rw [if_neg (not_le.mpr h_neg)]
      exact iterate_pred_toZ i hi

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

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + k = n

Tactic:
exact Nat.sub_add_cancel h

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x y : α
⊢ span {x, y} = span {x} ↔ x ∣ y

Tactic:
by
  rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]

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

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a • x * y + y * b ∈ I

Tactic:
smul_eq_mul,

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
IJ : I ≤ J
xJ : x ∈ J
left✝ : 1 ∉ I
oJ : 1 ∈ J
a b : α
h : b ∈ Submodule.span α ↑I
oe : 1 = a • x + b
F : y * 1 = y * (a • x + b)
⊢ a * x * y + y * b ∈ I
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ (a + b) ^ k ∈ I

Tactic:
hab.add_pow,

Goal state after:
α : Type u_6
inst✝ : Semiring α
I : Ideal α
a b : α
m n k : ℕ
ha : a ^ m ∈ I
hb : b ^ n ∈ I
hk : m + n ≤ k + 1
hab : Commute a b
⊢ ∑ m ∈ Finset.range (k + 1), a ^ m * b ^ (k - m) * ↑(k.choose m) ∈ I
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:
hIJ

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
⊢ x ∉ I → x ∈ J → 1 ∈ J
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ span {↑x ^ (n + 1)} ≤ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
rw [span_le, Set.singleton_subset_iff]

Goal state after:
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : ∑ a ∈ f.support, f a * ↑a = 1
this : 1 ∈ span ((fun i ↦ (f i * ↑i) ^ (n + 1)) '' ↑f.support)
x : ↑s
left✝ : x ∈ ↑f.support
⊢ ↑x ^ (n + 1) ∈ ↑(span ((fun x ↦ x ^ (n + 1)) '' s))
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst✝ : DivisionSemiring K
I✝ I : Ideal K
⊢ ![⊥, ⊤] ((fun I ↦ if I = ⊥ then 0 else 1) I) = I

Tactic:
rcases eq_bot_or_top I with rfl | rfl <;> simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y ∈ {s | ∃ a, a ∈ f ∧ ∃ b, b ∈ g ∧ s = a ∩ b}

Tactic:
refine ⟨a ∪ y, mem_of_superset ha subset_union_left, b ∪ y,
          mem_of_superset hb subset_union_left, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
f✝ g✝ : Filter α
s t : Set α
f g : Filter α
y a : Set α
ha : a ∈ f
b : Set α
hb : b ∈ g
xy : a ∩ b ⊆ y
⊢ y = (a ∪ y) ∩ (b ∪ y)
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case 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
hx : x ∈ submodule fun x ↦ f.range
⊢ x ∈ (mapRange.linearMap f).range

Tactic:
choose y hy using hx

Goal state after:
case 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
⊢ x ∈ (mapRange.linearMap f).range
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case 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
⊢ (x ∈ submodule fun x ↦ f.range) → x ∈ (mapRange.linearMap f).range

Tactic:
intro hx
    choose y hy using hx
    refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
    constructor
    <;> contrapose
    <;> simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
F : Filter α
G : Filter β
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
m✝ : α → β
m' : β → γ
s : Set α
t : Set β
m : α → β
f : Filter α
s₁ : Set α
h₁ : s₁ ∈ f.sets
s₂ : Set α
h₂ : s₂ ∈ f.sets
⊢ kernImage m s₁ ∩ kernImage m s₂ ∈ kernImage m '' f.sets

Tactic:
exact ⟨s₁ ∩ s₂, f.inter_sets h₁ h₂, Set.preimage_kernImage.u_inf⟩

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
s' : Set α
⊢ (𝓟 s' ⊓ l).HasBasis p fun i ↦ s' ∩ s i

Tactic:
simpa only [inf_comm, inter_comm] using hl.inf_principal s'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : β → Set α
S : Set β
h : Directed (fun x1 x2 ↦ x1 ⊇ x2) (s ∘ Subtype.val)
ne : S.Nonempty
t : Set α
⊢ ∀ ⦃x y : Set α⦄, x ⊇ y → 𝓟 x ≥ 𝓟 y

Tactic:
exact fun _ _ => principal_mono.2

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

Goal state before:
pp: α : Type u
f : Filter α
P : α → Prop
⊢ (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Tactic:
simp only [frequently_iff_forall_eventually_exists_and, @and_comm (P _),
    Set.ofPred_bijective.surjective.forall, Filter.Eventually, mem_ofPred]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
pa : ι → Prop
sa : ι → Set α
lb : Filter β
f : α → β
hla : la.HasBasis pa sa
⊢ Tendsto f la lb ↔ ∀ t ∈ lb, ∃ i, pa i ∧ MapsTo f (sa i) t

Tactic:
by
  simp only [Tendsto, (hla.map f).le_iff, image_subset_iff]
  rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (α → γ)
hs✝ : s ∈ (map (fun x1 x2 ↦ x1 ∘ x2) h).seq g
t : Set α
ht : t ∈ x
u : Set ((α → β) → α → γ)
hu✝ : u ∈ map (fun x1 x2 ↦ x1 ∘ x2) h
v : Set (α → β)
hv : v ∈ g
hs : u.seq v ⊆ s
w : Set (β → γ)
hw : w ∈ h
hu : (fun x1 x2 ↦ x1 ∘ x2) '' w ⊆ u
⊢ s.seq t ∈ h.seq (g.seq x)

Tactic:
grw [← hs, ← hu]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
⊢ h.seq (g.seq x) = ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
refine le_antisymm (le_seq fun s hs t ht => ?_) (le_seq fun s hs t ht => ?_)
  · rcases mem_seq_iff.1 hs with ⟨u, hu, v, hv, hs⟩
    rcases mem_map_iff_exists_image.1 hu with ⟨w, hw, hu⟩
    grw [← hs, ← hu]
    rw [← Set.seq_seq]
    exact seq_mem_seq hw (seq_mem_seq hv ht)
  · rcases mem_seq_iff.1 ht with ⟨u, hu, v, hv, ht⟩
    grw [← ht]
    rw [Set.seq_seq]
    exact seq_mem_seq (seq_mem_seq (image_mem_map hs) hu) hv

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

Goal state before:
pp: α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ IsDirected ↑s fun x1 x2 ↦ x1 ≤ x2

Tactic:
← directed_id_iff

Goal state after:
α : Type u_3
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
s : Set α
h : Ici a ⊆ s
f : α → α → α
hl : ∀ (a b : α), a ≤ f a b
hr : ∀ (a b : α), b ≤ f a b
this : Directed (fun x1 x2 ↦ x1 ≤ x2) Subtype.val
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) id
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R✝ : Type u_1
M : Type u_2
inst✝² : Semiring R✝
inst✝¹ : AddCommMonoid M
inst✝ : Module R✝ M
P Q R : { P // P.FG }
hPR : P ≤ R
hQR : Q ≤ R
⊢ ⟨↑P ⊔ ↑Q, ⋯⟩ ≤ R

Tactic:
rw [← Subtype.coe_le_coe] at hPR hQR ⊢
    exact sup_le hPR hQR

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
⊢ a • b₁ ≤ a • b₂

Tactic:
obtain ha | ha := ha.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 = a
⊢ a • b₁ ≤ a • b₂

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
obtain ha | ha := ha.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 = a
⊢ b₁ < b₂

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : a < 0
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

pp: case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0 • b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

pp: case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
· refine Or.inr ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonpos_of_nonneg ha.le hb

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0 • b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
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₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
⊢ Module.Finite A₂ B₂

Tactic:
let e : B₁ ≃ₐ[A₂] B₂ :=
    { e₂ with
      commutes' := fun r ↦ by
        simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm r) }

Goal state after:
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₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Module.Finite A₂ B₂
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
⊢ ∃ b ∈ t, Ici b ∩ t ⊆ s

Tactic:
by_contra! H

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
h : DirSupInaccOn D s
t : Set α
hD : t ∈ D
ht₀ : t.Nonempty
ht₁ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
ha : IsLUB t a
has : a ∈ s
H : ∀ b ∈ t, ¬Ici b ∩ t ⊆ s
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ o.brange f → a ∈ range (familyOfBFamily' r ho f)

Tactic:
rintro ⟨i, hi, rfl⟩

Goal state after:
case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
i : Ordinal.{u}
hi : i < o
⊢ f i hi ∈ range (familyOfBFamily' r ho f)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ (type r).brange (bfamilyOfFamily' r f) → a ∈ range f

Tactic:
rintro ⟨i, hi, rfl⟩

Goal state after:
case refine_1
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
i : Ordinal.{u}
hi : i < type r
⊢ bfamilyOfFamily' r f i hi ∈ range f
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i + 1 ≤ f j

Tactic:
add_one_le_iff

Goal state after:
case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
i j : β
hj : i < j
⊢ f i < f j
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
    Sum.Lex r emptyRelation a b →
      s (Sum.recOn a ⇑f.toRelEmbedding fun x ↦ f.top) (Sum.recOn b ⇑f.toRelEmbedding fun x ↦ f.top)

Tactic:
simpa [f.map_rel_iff] using f.lt_top

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

Goal state before:
pp: case refine_2
s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
ha : ∀ b < o, enumOrd s b ≤ a
b : Ordinal.{u}
hb : b < o
⊢ enumOrd s (succ b) ≤ ⨆ b, enumOrd s ↑b

Tactic:
exact Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)

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

Goal state before:
pp: case succ.inr
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
ih₂ : (b * b) ^ (go n (b * b) fuel).snd ≤ n
ih₃ : n < (b * b) ^ ((go n (b * b) fuel).snd + 1)
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]

Goal state after:
case succ.inr
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (b ^ 2) fuel).fst = n / b ^ (2 * (go n (b ^ 2) fuel).snd)
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) ≤ n
ih₃ : n < b ^ (2 * (go n (b ^ 2) fuel).snd + 2)
⊢ (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
          (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
        else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).fst =
      n /
        b ^
          (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
            else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd ∧
    b ^
          (if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
            else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd ≤
        n ∧
      n <
        b ^
          ((if n < b ^ (2 * (go n (b ^ 2) fuel).snd + 1) then
                (n / b ^ (2 * (go n (b ^ 2) fuel).snd), 2 * (go n (b ^ 2) fuel).snd)
              else (n / b ^ (2 * (go n (b ^ 2) fuel).snd + 1), 2 * (go n (b ^ 2) fuel).snd + 1)).snd +
            1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case h₂
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v + 1 ≤ b ^ (log b v + 1)

Tactic:
add_one_le_iff

Goal state after:
case h₂
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ v < b ^ (log b v + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ nfp (fun x ↦ a * x) 0 = 0

Tactic:
rw [← nonpos_iff_eq_zero, nfp_le_iff]
  simp

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

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

Tactic:
← ord_le_ord,

Goal state after:
o : Ordinal.{u_1}
ho : o.IsInitial
c : Cardinal.{u_1}
⊢ o ≤ c.ord ↔ o.card.ord ≤ c.ord