mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / (b * e) ≤ c / (d * e)

Tactic:
div_mul_eq_div_mul_one_div,

Goal state after:
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
inst✝ : IsStrictOrderedRing α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / (d * e)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b = (a = b)

Tactic:
apply propext

Goal state after:
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b ↔ a = b
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ 0 < b ∧ a ≤ b ∨ b = 0 ∨ b < 0 ∧ b ≤ a

Tactic:
simp [hb, hb.not_gt, hb.ne, div_le_one_of_neg]

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons_cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
⊢ ∀ {l₁ : List α}, Forall₂ R l₁ (a✝¹ :: l₁✝) → SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
| cons_cons _ _ ih =>

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → α
l₁ : List γ
l₂ : List β
⊢ SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b ↦ R (f c) b) l₁ l₂

Tactic:
by
  simp [sublistForall₂_iff]

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
rintro ⟨l1, h1, h2⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
l1 : List β
h1 : Forall₂ R l₁ l1
h2 : l1 <+ map f l₂
⊢ ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
rintro ⟨l1, h1, h2⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ l1 : List γ
h1 : Forall₂ (fun a c ↦ R a (f c)) l₁ l1
h2 : l1 <+ l₂
⊢ ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c ↦ R a (f c)) l₁ l₂

Tactic:
by
  simp only [sublistForall₂_iff]
  constructor
  · rintro ⟨l1, h1, h2⟩
    obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
    use l'
    simpa [hl1] using h1
  · rintro ⟨l1, h1, h2⟩
    use l1.map f
    simp [h1, h2.map]

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)

Tactic:
apply propext

Goal state after:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
apply propext

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Tactic:
· exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take (i + 1) L).prod = (take i L).prod * L[i]

Tactic:
by
  rw [← take_concat_get' _ _ p, prod_append]
  simp

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l l' : List M
h : l.length = l'.length
⊢ l.prod * l'.prod = (zipWith (fun x1 x2 ↦ x1 * x2) l l').prod

Tactic:
apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans
  rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case pos
α : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
p : α → Prop
inst✝ : DecidablePred p
f g : α → M
x : α
xs : List α
hx : p x
⊢ (if p x then f x else g x) *
      ((map f (filter (fun b ↦ decide (p b)) xs)).prod * (map g (filter (fun a ↦ decide ¬p a) xs)).prod) =
    (map f
          (if decide (p x) = true then x :: filter (fun b ↦ decide (p b)) xs
          else filter (fun b ↦ decide (p b)) xs)).prod *
      (map g
          (if (decide ¬p x) = true then x :: filter (fun a ↦ decide ¬p a) xs else filter (fun a ↦ decide ¬p a) xs)).prod

Tactic:
simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]

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

Goal state before:
pp: case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂

Tactic:
rintro ⟨rfl, rfl, rfl⟩
    rfl

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

Goal state before:
pp: case neg
x : ℤ
hx : x ≠ 0
n d : ℤ
hd : ¬d = 0
⊢ n /. x * (x /. d) = n /. d

Tactic:
rw [divInt_mul_divInt, x.mul_comm, divInt_mul_right hx]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Rat

Goal state before:
pp: a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ∧ ¬↑c / ↑d ≤ ↑a / ↑b ↔ a * d ≤ c * b ∧ ¬c * b ≤ a * d

Tactic:
apply and_congr

Goal state after:
case h₁
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ↑a / ↑b ≤ ↑c / ↑d ↔ a * d ≤ c * b

case h₂
a b c d : ℤ
b_pos : 0 < b
d_pos : 0 < d
⊢ ¬↑c / ↑d ≤ ↑a / ↑b ↔ ¬c * b ≤ a * d
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m → n ≤ m

Tactic:
intro h
    rw [← not_lt]
    intro hmn
    apply ha
    have : a ^ m * a ∣ a ^ m * 1 := by
      rw [← pow_succ, mul_one]
      exact (pow_dvd_pow _ (Nat.succ_le_of_lt hmn)).trans h
    rwa [mul_dvd_mul_iff_left, ← isUnit_iff_dvd_one] at this
    apply pow_ne_zero m ha₀

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
b0 : b ≠ 0
⊢ (a /. b).num ∣ a

Tactic:
by
  rcases e : a /. b with ⟨n, d, h, c⟩
  rw [Rat.mk_eq_divInt, divInt_eq_divInt_iff b0 (mod_cast h)] at e
  refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <|
    c.dvd_of_dvd_mul_right ?_
  have := congr_arg Int.natAbs e
  simp only [Int.natAbs_mul, Int.natAbs_natCast] at this; simp [this]

Goal state after:
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ n1 * (e1 * (n2 / e2)) = t1

Tactic:
h2,

Goal state after:
α : Type u_1
inst✝ : Field α
n1 n2 k e1 e2 t1 : α
h1 : n1 * e1 = t1
h2 : n2 / e2 = 1
h3 : n1 * n2 = k
⊢ n1 * (e1 * 1) = t1
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : 0 < ad
hbd : 0 < bd
hgcd : 0 < gcd
⊢ 0 < 1 / gcd

Tactic:
· exact one_div_pos.2 hgcd

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Canonical

Goal state before:
pp: case inl
R : Type u
inst✝³ : CommSemiring R
inst✝² : PartialOrder R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : PosMulStrictMono R
a b d : R
hab : a < b
this : MulPosStrictMono R
hcd : 0 < d
⊢ 0 < b * d

Tactic:
exact mul_pos hab.pos hcd

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ

Tactic:
le_compl_iff_le_compl,

Goal state after:
α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ l bᶜ ≤ aᶜ
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: β : Type u_2
ι : Type u_12
t : Set ι
s : ι → Set β
w : ⋃ i ∈ t, s i = ⊤
x : β
p : ∃ i, x ∈ ⋃ (_ : i ∈ t), s i
⊢ ∃ i ∈ t, x ∈ s i

Tactic:
simpa using p

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
S : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
h : ∀ x ∈ S, DirectedOn r x
⊢ DirectedOn r (⋃₀ S)

Tactic:
by
  rw [sUnion_eq_iUnion]
  exact directedOn_iUnion (directedOn_iff_directed.mp hd) (fun i ↦ h i.1 i.2)

Goal state after:
Module: Mathlib.Order.LatticeIntervals

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : Lattice α
inst✝ : OrderBot α
⊢ ComplementedLattice ↑(Iic a) ↔ ∀ b ≤ a, ∃ c ≤ a, b ⊓ c = ⊥ ∧ b ⊔ c = a

Tactic:
simp_rw [complementedLattice_iff, Iic.isCompl_iff, Subtype.forall, Subtype.exists, disjoint_iff,
    exists_prop, Set.mem_Iic]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : Coframe β
⊢ Coframe α

Tactic:
let completeLattice := e.completeLattice
  let coheytingAlgebra := e.coheytingAlgebra
  apply e.injective.coframe <;> intros <;> first | rfl | exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
a : α
inst✝ : Std.Symm r
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b

Tactic:
simp only [pairwise_insert, Std.Symm.iff a, and_self_iff]

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S = ∅
⊢ IsGLB S ⟨b, ⋯⟩

pp: case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsGLB S ⟨sInf (Subtype.val '' S), ⋯⟩

Tactic:
· subst hS; simp only [isGLB_empty_iff, isTop_iff_eq_top]; rfl

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsGLB S ⟨sInf (Subtype.val '' S), ⋯⟩
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
⊢ Disjoint (mulSupport (mulSingle i a)) (mulSupport (mulSingle j b)) ↔ i ≠ j

Tactic:
by
  rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]

Goal state after:
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
⊢ a ≤ b ↔ a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ

Tactic:
refine ⟨fun h ↦ ⟨oneLePart_mono h, leOnePart_anti h⟩, fun h ↦ ?_⟩

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a b : α
h : a⁺ᵐ ≤ b⁺ᵐ ∧ b⁻ᵐ ≤ a⁻ᵐ
⊢ a ≤ b
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case mp
n : ℕ
h : n ! = 1
⊢ n ≤ 1

Tactic:
← not_lt,

Goal state after:
case mp
n : ℕ
h : n ! = 1
⊢ ¬1 < n
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n) * (1 + n)! + 1 * (1 + n)!

Tactic:
Nat.one_mul,

Goal state after:
i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + n) * (1 + n)! + (1 + n)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

Tactic:
by_cases hkn : k ≤ n

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0

case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
hkn : ¬k ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑m = 2 * x
⊢ round x = m / 2

Tactic:
rcases m.even_or_odd with ⟨m, rfl⟩ | ⟨m, rfl⟩

Goal state after:
case inl.inl
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(m + m) = 2 * x
⊢ round x = (m + m) / 2

case inl.inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 2 * fract x ≠ 1
m : ℤ
hm : ↑(2 * m + 1) = 2 * x
⊢ round x = (2 * m + 1) / 2
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case succ.zero
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
IH : (h : 0 < 0) → p ⟨0, h⟩
h : 0 < 0 + 1
⊢ p ⟨0 + 1, h⟩

Tactic:
exact one

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

Goal state before:
pp: k m : ℕ+
⊢ k ∣ m ↔ m.mod k = k

Tactic:
by
  rw [dvd_iff]
  rw [Nat.dvd_iff_mod_eq_zero]; constructor
  · intro h
    apply PNat.eq
    rw [mod_coe, if_pos h]
  · intro h
    by_cases h' : (m : ℕ) % (k : ℕ) = 0
    · exact h'
    · replace h : (mod m k : ℕ) = (k : ℕ) := congr_arg _ h
      rw [mod_coe, if_neg h'] at h
      exact ((Nat.mod_lt (m : ℕ) k.pos).ne h).elim

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

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n) = min (↑(m % n) / ↑n) (↑(n - m % n) / ↑n)

Tactic:
Nat.cast_sub (m.mod_lt hn).le,

Goal state after:
case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (↑(m % n) / ↑n) (1 - ↑(m % n) / ↑n) = min (↑(m % n) / ↑n) ((↑n - ↑(m % n)) / ↑n)
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1

Tactic:
rw [← one_lt_inv'] at hlt

Goal state after:
case inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective fun x ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun x ↦ a ^ x) k
hb : (fun x ↦ a ^ x) k < 1
⊢ 0 < k ∧ k < 1
Module: Mathlib.Algebra.Order.Ring.Pow

Goal state before:

Tactic:
_ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
        le_add_of_nonneg_right <| by
          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
          two_mul, pow_zero, mul_one,
          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
        abel
      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
        gcongr
        apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
⊢ (↑n / ↑d).num / ↑(↑n / ↑d).den = n / ↑d

Tactic:
set q := (n : ℚ) / d with q_eq

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ q.num / ↑q.den = n / ↑d
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < c * ↑q.den

Tactic:
← d_eq_c_mul_denom,

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ 0 < ↑d
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
⊢ R (f x) (f y)

Tactic:
have ha' : 0 ≤ a := ha.le

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
⊢ R (f x) (f y)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = count a ⟦l⟧ - 1

Tactic:
convert! List.count_erase_self (a := a) (l := l)

Goal state after:
case e'_2
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a (erase ⟦l⟧ a) = List.count a (l.erase a)

case e'_3
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
l : List α
⊢ count a ⟦l⟧ = List.count a l
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s t : Multiset α
h : s < t
⊢ map f s < map f t

Tactic:
by
  refine (map_le_map h.le).lt_of_not_ge fun H => h.ne <| eq_of_le_of_card_le h.le ?_
  rw [← s.card_map f, ← t.card_map f]
  exact card_le_card H

Goal state after:
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

Tactic:
by_cases ha : a ∈ l

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.headI = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.headI else (a :: l).headI
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
by_cases ha : a ∈ l

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
ha : ¬a ∈ l
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
a : α
x✝ : List α
⊢ List.count a x✝.dedup = if a ∈ x✝ then 1 else 0

Tactic:
apply List.count_dedup _ _

Goal state after:
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case some
α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
b : β
h : f a = some b
⊢ filterMap f (a ::ₘ s) = (Option.map singleton (some b)).getD 0 + filterMap f s

Tactic:
| some b =>

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

Goal state before:
pp: α : Type u_1
p : Prop
inst✝ : Decidable p
s : Finset α
⊢ filter (fun _a ↦ p) s = if p then s else ∅

Tactic:
by split_ifs <;> simp [*]

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ Injective fun i ↦ f ↑i ⋯

Tactic:
intro ⟨i, hi⟩ ⟨j, hj⟩ eq

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
i : ℕ
hi : i ∈ range n
j : ℕ
hj : j ∈ range n
eq : (fun i ↦ f ↑i ⋯) ⟨i, hi⟩ = (fun i ↦ f ↑i ⋯) ⟨j, hj⟩
⊢ ⟨i, hi⟩ = ⟨j, hj⟩
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n) * n - 1 * n + (n - (↑i % n + 1))) % n

Tactic:
Nat.one_mul,

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n) * n - n + (n - (↑i % n + 1))) % n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin n
⊢ (last n).succAbove i = i.castSucc

Tactic:
by rw [succAbove_last]

Goal state after:
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: case refine_2
α : Type u
n : ℕ
f : Fin n → α
n✝ : ℕ
x₀ : α
xs : Fin n✝ → α
ih : (ofFn xs).Nodup → Function.Injective xs
⊢ (ofFn (Fin.cons x₀ xs)).Nodup → Function.Injective (Fin.cons x₀ xs)

Tactic:
intro h
    rw [Fin.cons_injective_iff]
    simp_rw [ofFn_succ, Fin.cons_succ, nodup_cons, Fin.cons_zero, mem_ofFn] at h
    exact h.imp_right ih

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
α : Sort u_1
n : ℕ
x₀ : Fin 1 → α
x : Fin n → α
i : Fin n
⊢ cons (x₀ 0) x i.succ = x i

Tactic:
exact Fin.cons_succ _ _ _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ Set.range Subtype.val

Tactic:
by
    rwa [Subtype.range_coe_subtype]

Goal state after:
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ hd :: tl <+ l'

Tactic:
rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
this : ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
⊢ [hd] ++ tl <+ take (f 0 + 1) l' ++ drop (f 0 + 1) l'