mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some ⋯.some ∈ ⋃ (_ : ⋯.some ∈ g ⁻¹' {k}), s ⋯.some

Tactic:
simp only [mem_preimage, mem_singleton_iff, mem_iUnion, exists_prop]

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ g ⋯.some = k ∧ hs.some ⋯.some ∈ s ⋯.some
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
· exact colorable_set_nonempty_of_colorable hc

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
k : ℕ
u v : V
inst✝ : Fintype ↑(G.neighborSet u)
h : G.IsEdgeReachable k u v
huv : u ≠ v
⊢ k ≤ G.degree u

Tactic:
by
  classical
  by_contra! hh
  rw [← card_incidenceSet_eq_degree, ← ENat.natCast_lt_natCast, Set.coe_fintypeCard] at hh
  obtain ⟨w, _⟩ := h hh |>.exists_isPath
  simpa using w.adj_snd <| mt Walk.Nil.eq huv

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w x y z : V
h : G.Adj x y
p' : G.Walk y z
ih : w ∈ p'.toSubgraph.verts ↔ w ∈ p'.support
this : w = y ∨ w ∈ p'.support ↔ w ∈ p'.support
⊢ w ∈ (cons h p').toSubgraph.verts ↔ w ∈ (cons h p').support

Tactic:
simp [ih, or_assoc, this]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this✝¹ : G.dist v w = 1
this✝ : G.dist w v = 1
this : G.dist u w ≤ G.dist u v + G.dist v w
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
have : G.dist u v ≤ G.dist u w + G.dist w v := huw.dist_triangle_left v

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this✝² : G.dist v w = 1
this✝¹ : G.dist w v = 1
this✝ : G.dist u w ≤ G.dist u v + G.dist v w
this : G.dist u v ≤ G.dist u w + G.dist w v
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.IsPath

Tactic:
rw [← this]

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.bypass.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ (circulantGraph s).Adj u v ↔ (circulantGraph (s \ {0})).Adj u v

Tactic:
simp only [circulantGraph, fromRel_adj, and_congr_right_iff]

Goal state after:
G : Type u_1
inst✝ : AddGroup G
s : Set G
u v : G
⊢ u ≠ v → (u - v ∈ s ∨ v - u ∈ s ↔ u - v ∈ s \ {0} ∨ v - u ∈ s \ {0})
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
⊢ (∃ G x, G.IsExtremal p) ↔ ∃ G, p G

Tactic:
by
  classical
  refine ⟨fun ⟨_, _, h⟩ ↦ ⟨_, h.1⟩, fun ⟨G, hp⟩ ↦ ?_⟩
  obtain ⟨G', hp', h⟩ := by
    apply exists_max_image { G | p G } (#·.edgeFinset)
    use G, by simpa using hp
  use G', inferInstanceAs (DecidableRel G'.Adj)
  exact ⟨by simpa using hp', fun _ _ hp ↦ by convert! h _ (by simpa using hp)⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝¹ : Nonempty V
inhabited_h : Inhabited V
this✝ : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : ((f a).firstDart ⋯).edge = ((f b).firstDart ⋯).edge
this :
  ∀ (a : V) (ha : a ∈ {default}ᶜ) (b : V) (hb : b ∈ {default}ᶜ),
    ((f a).firstDart ⋯).edge = ((f b).firstDart ⋯).edge → (f a).length ≤ (f b).length → a = b
h' : ¬(f a).length ≤ (f b).length
⊢ a = b

pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : ((f a).firstDart ⋯).edge = ((f b).firstDart ⋯).edge
h' : (f a).length ≤ (f b).length
⊢ a = b

Tactic:
· exact Eq.symm (this _ hb _ ha h.symm (le_of_not_ge h'))

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
f : (x : V) → G.Walk x default
hf : ∀ (x : V), (fun p ↦ p.IsPath) (f x)
hf' : ∀ (x : V) (y : G.Walk x default), (fun p ↦ p.IsPath) y → y = f x
a : V
ha : a ∈ {default}ᶜ
b : V
hb : b ∈ {default}ᶜ
h : ((f a).firstDart ⋯).edge = ((f b).firstDart ⋯).edge
h' : (f a).length ≤ (f b).length
⊢ a = b
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
⊢ G.minDegree = 1

Tactic:
have := h.card_edgeFinset

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
h : G.IsTree
inst✝² : Fintype V
inst✝¹ : Nontrivial V
inst✝ : DecidableRel G.Adj
q : 2 ≤ G.minDegree
this : G.edgeFinset.card + 1 = Fintype.card V
⊢ G.minDegree = 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
⊢ ⨆ k, C.labelGraph k = G

Tactic:
by
  ext x y
  simp only [iSup_adj, EdgeLabeling.labelGraph_adj]
  grind

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1
α : Type u
G : SimpleGraph α
s : Set α
r t : ℕ
v : Fin r × Fin t
⊢ ↑(⟨↑v.1 % r, ⋯⟩, ⟨↑⟨↑v.2 * r + ↑v.1, ⋯⟩ / r, ⋯⟩).1 = ↑v.1

Tactic:
exact Nat.mod_eq_of_lt v.1.prop

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
w✝ : Fin (Fintype.card V)
p : G.Walk u v
h✝ : p ∈ G.finsetWalkLength (↑w✝) u v
⊢ G.Reachable u v

Tactic:
exact ⟨p⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ G.Preconnected ∧ univ.Nonempty ↔ G.Connected

Tactic:
by
    rw [connected_iff, ← Finset.univ_nonempty_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case h
n r c : ℕ
hr : r > 0
⊢ c % r = (r * n + c) % r

Tactic:
Nat.mul_add_mod_self_left

Goal state after:
case h
n r c : ℕ
hr : r > 0
⊢ c % r = c % r
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ G.diam = (⨆ p, G.edist p.1 p.2).toNat

Tactic:
rw [diam, ediam_def]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: case inl
n : ℕ
⊢ #(turanGraph n 0).edgeFinset = (n ^ 2 - (n % 0) ^ 2) * (0 - 1) / (2 * 0) + (n % 0).choose 2

Tactic:
rw [Nat.mod_zero, tsub_self, zero_mul, Nat.zero_div, zero_add]

Goal state after:
case inl
n : ℕ
⊢ #(turanGraph n 0).edgeFinset = n.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case neg.refine_2.refine_2
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : ¬t = 0
x✝ : ∃ K s, #s = t ∧ ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
K : G.CompleteEquipartiteSubgraph r t
s : Finset V
hs : #s = t
hadj : ∀ p ∈ K.parts, G.IsCompleteBetween ↑p ↑s
⊢ r + 1 = r + 1 ∨ t = 0

Tactic:
exact .inl rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
⊢ ⊤.egirth = 3

Tactic:
refine le_antisymm ?_ three_le_egirth
  obtain ⟨s, hcard⟩ := Cardinal.exists_finset_eq_card <| Cardinal.ofNat_le_toENat.mp h
  obtain ⟨x, y, z, hxy, hxz, hyz, -⟩ := s.card_eq_three.mp hcard.symm
  set w : Walk ⊤ x x := .cons hxy <| .cons hyz <| .cons hxz.symm .nil with hw
  have : w.IsCycle :=
    { edges_nodup := by aesop
      ne_nil := by aesop
      support_nodup := by aesop }
  grw [egirth_le_length this]
  simp [hw]

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

Goal state before:
pp: case inr
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ ∃ t u, t ∪ u = s ∧ Disjoint t u ∧ #↑t = #↑u

Tactic:
classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t, u
  simp [← Finset.coe_union, *]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
⊢ ‖Fin (r + 1)‖ ≤ #(insert w₁ s)

Tactic:
simp [hw.isNClique_fst_left.2]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i

Tactic:
have ⟨u, he, _⟩ := h hv

Goal state after:
case refine_1
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
u : V
he : (fun w ↦ M.Adj v w) u
right✝ : ∀ (y : V), (fun w ↦ M.Adj v w) y → y = u
⊢ ∃ i, ∃ (_ : i ∈ M.edgeSet), v ∈ ↑i
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
w : V
hvw : M.Adj v✝ w
hw : ∀ (y : V), (fun w ↦ M.Adj v✝ w) y → y = w
⊢ (fun w ↦ (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) w ∧
    ∀ (y : V), (fun w ↦ (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) y → y = w

Tactic:
simpa [hv, hvw, M.edge_vert hvw.symm, (M.adj_sub hvw).symm.reachable] using fun _ _ _ ↦ hw _

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ Nonempty (↑t ≃ ↑u)

Tactic:
rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
      ← u.cast_ncard (Set.finite_union.mp hu).2]

Goal state after:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ ↑t.ncard = ↑u.ncard
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(G.degree i) = ∑ j, if G.Adj i j then 1 else 0

Tactic:
unfold degree neighborFinset neighborSet

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
R : Type u_3
inst✝ : AddCommMonoidWithOne R
i : V
⊢ ↑(#{w | G.Adj i w}.toFinset) = ∑ j, if G.Adj i j then 1 else 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = c.supp

Tactic:
rw [← this]

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
this : p.toSubgraph.verts = c.supp
⊢ (p.rotate v hvp).IsCycle ∧ (p.rotate v hvp).toSubgraph.verts = p.toSubgraph.verts
Module: Mathlib.Combinatorics.SimpleGraph.VertexCover

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
h : G.vertexCoverNum = 0
⊢ G = ⊥

Tactic:
simpa [h] using vertexCoverNum_exists G

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: ε : ℝ
hε : 0 < ε
r t : ℕ
hr_pos : 0 < r
ht_pos : 0 < t
ε' : ℝ := 1 / (↑(r - 1) * ↑r) + ε
hε' : 0 < ε'
t' : ℕ := ⌊↑t / (↑r * ε)⌋₊ + 1
ht_lt_rt'ε : ↑t < ↑r * ↑t' * ε
ht'_pos : 0 < t'
N' : ℕ
N : ℕ := max (max 1 N') ⌈(↑(t'.choose t) ^ r * ↑t + ↑r * ↑t') * (↑t' - ↑t) / (↑r * ↑t' * ε - ↑t)⌉₊
n : ℕ
hn : N ≤ n
G : SimpleGraph (Fin n)
x✝ : DecidableRel G.Adj
hδ : ↑G.minDegree ≥ (1 - 1 / ↑r + ε) * ↑n
this : Nonempty (Fin n)
hrε_lt_1 : ↑r * ε < 1
ht_lt_t' : t < t'
ih : completeEquipartiteGraph r t' ⊑ G
K : G.CompleteEquipartiteSubgraph r t'
y : (a : Finset (Fin n)) → a ∈ K.parts → Finset (Fin n)
hy✝ : y ∈ K.parts.pi fun x ↦ powersetCard t x
hy : ∀ (a : Finset (Fin n)) (h : a ∈ K.parts), y a h ∈ powersetCard t a
ht_le_card_filter : t ≤ #{w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
s : Finset ↥(ErdosStone.filter K t)
hs_subset : s ⊆ {w | ErdosStone.filter.pi K w = ⟨y, hy✝⟩}
hcards : #s = t
K' : G.CompleteEquipartiteSubgraph r t :=
  { parts := Finset.map { toFun := fun p ↦ y ↑p ⋯, inj' := ⋯ } univ, card_parts := ⋯, card_mem_parts := ⋯,
    isCompleteBetween := ⋯ }
⊢ #(Finset.map (Function.Embedding.subtype fun x ↦ x ∈ ErdosStone.filter K t) s) = t

Tactic:
rwa [← card_map] at hcards

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
x✝ : pt₁.index = pt₂.index ∧ ∃ g, ⟦g⟧ = pt₁.groupElts ∧ ⟦g⟧ = pt₂.groupElts
h : pt₁.index = pt₂.index
g : G
hg₁ : ⟦g⟧ = pt₁.groupElts
hg₂ : ⟦g⟧ = pt₂.groupElts
⊢ pt₁ = pt₂

Tactic:
· rcases pt₁ with ⟨i₁, g₁⟩
    rcases pt₂ with ⟨i₂, g₂⟩
    dsimp only at h
    subst h
    ext
    · rfl
    · exact heq_of_eq (hg₁.symm.trans hg₂)

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ g • x ∈ ↑(g • pt) ↔ x ∈ pt

Tactic:
coe_smul,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ g • x ∈ g • ↑pt ↔ x ∈ pt
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ ↑(g • pt) ↔ g⁻¹ • x ∈ ↑pt

Tactic:
coe_smul,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g • ↑pt ↔ g⁻¹ • x ∈ ↑pt
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ ↑(g⁻¹ • pt) ↔ g • x ∈ ↑pt

Tactic:
coe_smul,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g⁻¹ • ↑pt ↔ g • x ∈ ↑pt
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: case mk
μ : YoungDiagram
T' : SemistandardYoungTableau μ
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, (i, j) ∉ μ → entry✝ i j = 0
h : { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry = T'.entry
⊢ { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ } = T'

Tactic:
cases T'

Goal state after:
case mk.mk
μ : YoungDiagram
entry✝¹ : ℕ → ℕ → ℕ
row_weak'✝¹ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝¹ i j1 ≤ entry✝¹ i j2
col_strict'✝¹ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝¹ i1 j < entry✝¹ i2 j
zeros'✝¹ : ∀ {i j : ℕ}, (i, j) ∉ μ → entry✝¹ i j = 0
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, (i, j) ∉ μ → entry✝ i j = 0
h :
  { entry := entry✝¹, row_weak' := row_weak'✝¹, col_strict' := col_strict'✝¹, zeros' := zeros'✝¹ }.entry =
    { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry
⊢ { entry := entry✝¹, row_weak' := row_weak'✝¹, col_strict' := col_strict'✝¹, zeros' := zeros'✝¹ } =
    { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: p : ℕ
⊢ unpaired (fun z n ↦ Nat.rec (id z) (fun y IH ↦ (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2.succ) n) p =
    unpaired (fun x1 x2 ↦ x1 + x2) p

Tactic:
simp; induction p.unpair.2 <;> simp [*, Nat.add_assoc]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Primcodable α
inst✝¹ : Primcodable β
p : β → Prop
inst✝ : DecidablePred p
hp : PrimrecPred p
f : α → Subtype p
⊢ (Primrec fun a ↦ ↑(f a)) ↔ Primrec f

Tactic:
by
  let := Primcodable.subtype hp
  refine ⟨fun h => ?_, fun hf => subtype_val.comp hf⟩
  refine Nat.Primrec.of_eq h fun n => ?_
  rcases @decode α _ n with - | a; · rfl
  simp; rfl

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: p : ℝ
hp : p ≠ 0
⊢ (fun x ↦ ‖deriv (fun z ↦ z ^ p * (1 - ε z)) x‖) =Θ[atTop] fun z ↦ z ^ (p - 1)

Tactic:
by
  refine IsTheta.norm_left ?_
  calc (fun x => deriv (fun z => z ^ p * (1 - ε z)) x) =Θ[atTop] fun z => p * z ^ (p - 1) :=
        (isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn hp).isTheta
    _ =Θ[atTop] fun z => z ^ (p - 1) := IsTheta.const_mul_left hp <| isTheta_refl _ _

Goal state after:
Module: Mathlib.Computability.AkraBazzi.AkraBazzi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)

Tactic:
have hb_lt_one : b' < 1 := calc b (min_bi b) / 2
    _ < b (min_bi b) := div_two_lt_of_pos (R.b_pos (min_bi b))
    _ < 1 := R.b_lt_one (min_bi b)

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
q : ℝ → ℝ
hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)
hq_poly : GrowsPolynomially fun x ↦ ‖deriv q x‖
i : α
b' : ℝ := b (min_bi b) / 2
hb_pos : 0 < b'
hb_lt_one : b' < 1
⊢ (fun n ↦ q ↑(r i n) - q (b i * ↑n)) =O[atTop] fun n ↦ deriv q ↑n * (↑(r i n) - b i * ↑n)
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ (fun n ↦ ε (b i * ↑n) - ε ↑n) =Θ[atTop] fun n ↦ 1 / log ↑n ^ 2

Tactic:
by
  calc (fun (n : ℕ) => ε (b i * n) - ε n)
    _ =Θ[atTop] fun n => (-log (b i)) / (log n) ^ 2 :=
      (R.isEquivalent_smoothingFn_sub_self i).isTheta
    _ = fun (n : ℕ) => (-log (b i)) * 1 / (log n) ^ 2 := by simp only [mul_one]
    _ = fun (n : ℕ) => -log (b i) * (1 / (log n) ^ 2) := by simp_rw [← mul_div_assoc]
    _ =Θ[atTop] fun (n : ℕ) => 1 / (log n) ^ 2 := by
      have : -log (b i) ≠ 0 := by
        rw [neg_ne_zero]
        exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
      rw [← isTheta_const_mul_right this]

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:

Tactic:
0 < (n : ℝ) ^ p a b * (1 + 0) := by aesop (add safe Real.rpow_pos_of_pos)
       _ ≤ asympBound g a b n := by
        simp only [asympBound_def']
        gcongr n ^ p a b * (1 + ?_)
        have := R.g_nonneg
        aesop (add safe Real.rpow_nonneg, safe div_nonneg, safe Finset.sum_nonneg)

Goal state after:
Module: Mathlib.Computability.AkraBazzi.GrowsPolynomially

Goal state before:
pp: f : ℝ → ℝ
hf : GrowsPolynomially f
h : ∀ᶠ (x : ℝ) in atTop, f x ≠ 0
h' : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ ∀ᶠ (x : ℝ) in atTop, 0 ≠ f x

Tactic:
by filter_upwards [h] with x hx; exact hx.symm

Goal state after:
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, g ↑u / ↑u ^ (p a b + 1) ≤
    ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, c₂ * g ↑n / ↑u ^ (p a b + 1)

Tactic:
gcongr with u hu

Goal state after:
case hab
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ g ↑u ≤ c₂ * g ↑n
Module: Mathlib.Computability.AkraBazzi.SumTransform

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
⊢ ↑n ^ p a b * ∑ u ∈ Ico (r i n) n, c₂ * g ↑n / ↑u ^ (p a b + 1) ≤
    ↑n ^ p a b * ∑ _u ∈ Ico (r i n) n, c₂ * g ↑n / ↑(r i n) ^ (p a b + 1)

Tactic:
gcongr with u hu

Goal state after:
case a
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
c₁ : ℝ
hc₁_mem : c₁ ∈ Set.Ioo 0 1
hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
c₂ : ℝ
hc₂_mem : c₂ > 0
hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hc₁_pos : 0 < c₁
n : ℕ
hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)
hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n
hrpos : ∀ (i : α), 0 < r i n
hr_lt_n : ∀ (i : α), r i n < n
hn_pos : 0 < n
i : α
hrpos_i : 0 < r i n
g_nonneg : 0 ≤ g ↑n
hp : 0 ≤ p a b + 1
u : ℕ
hu : u ∈ Ico (r i n) n
⊢ r i n ≤ u